proposition: Lemma equiv_hlist_Hcons : forall ls i a b (c : hlist ls) d, equiv_hlist (Hcons a c) (@Hcons i ls b d) -> (@eqv i a b /\ equiv_hlist c d).
proof: Proof. clear. intros. refine match H in @equiv_hlist ls' l r return match ls' as ls' return hlist ls' -> hlist ls' -> _ with | nil => fun _ _ => True | l :: ls => fun l r => eqv (hlist_hd l) (hlist_hd r) /\ equiv_hlist (hlist_tl l) (hlist_tl r) end l r with | hlist_eqv_nil => I | hlist_eqv_cons _ _ _ _ _ _ pf pf' => conj pf pf' end. Defined.
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