proposition: Lemma hcons_paths {A: UU} (x y: A) {n: nat} (v: vec UU n) (xs ys: hvec v) (p: x = y) (ps: xs = ys) : x ::: xs = y ::: ys.
proof: Proof. apply (map_on_two_paths (λ x xs, @hcons A x n v xs)) ; assumption. Defined.
imports: UniMath.Foundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors