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