proposition: Lemma append_comm_cons {A : Type} {n1 n2 : nat} (v1 : t A n1) (v2 : t A n2) (a : A) : cons a (append v1 v2) = append (cons a v1) v2.
proof: Proof. simpl. reflexivity. Defined.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy Param_nat