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