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. apply (map_on_two_paths (λ x xs, @hcons A x n v xs)) ; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.