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