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