proposition: Lemma iapp_hetero_cong {n' m'} (v : ilist A n) (v' : ilist A n') (w : ilist A m) (w' : ilist A m') : hetero_veq v v' -> hetero_veq w w' -> hetero_veq (iapp v w) (iapp v' w').
proof: Proof. red. intros [eq Heq]. depelim eq. destruct Heq. intros [eq Heq]. depelim eq. destruct Heq. exists refl_equal. constructor. Defined.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations