proposition: Lemma equiv_hlist_app : forall a b (c c' : hlist a) (d d' : hlist b), (equiv_hlist c c' /\ equiv_hlist d d') <-> equiv_hlist (hlist_app c d) (hlist_app c' d').
proof: Proof. clear. split. - destruct 1. induction H. + assumption. + simpl. constructor; auto. - induction c. + rewrite (hlist_eta c'). simpl; intros; split; auto. constructor. + rewrite (hlist_eta c'); simpl. specialize (IHc (hlist_tl c')). intro. eapply equiv_hlist_Hcons in H. intuition. constructor; auto. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.Member ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics Coq.Classes.Morphisms