proposition: Lemma hetero_veq_transport_right {A} {n m} (v : ilist A n) (w : ilist A m) (eq : m = n) : hetero_veq v w -> hetero_veq v (eq # w).
proof: Proof. destruct eq. simpl. trivial. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations