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