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