Theorem cons_inj1 {A: UU} (a1 a2: A) (r1 r2: list A) : a1 :: r1 = a2 :: r2 → a1 = a2. Proof. intro H. apply (maponpaths head) in H. change (just a1 = just a2) in H. apply ii1_injectivity in H. assumption. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.