proposition: Theorem equiv_eq_eq : forall ls (x y : hlist ls), equiv_hlist (fun x => @eq _) x y <-> x = y.
proof: Proof. induction x; simpl; intros. { split. inversion 1. rewrite hlist_nil_eta. reflexivity. intros; subst; constructor. } { split. { intro. rewrite (hlist_eta y). specialize (IHx (hlist_tl y)). refine (match H in @equiv_hlist _ LS X Y return match X in hlist LS return F match LS with | nil => l | l :: _ => l end -> hlist match LS with | nil => ls | _ :: ls => ls end -> Prop with | Hnil => fun _ _ => True | Hcons a b c d => fun x y => (equiv_hlist (fun x0 : iT => eq) d y <-> d = y) -> @Hcons a b c d = Hcons x y end (match LS as LS return hlist LS -> F match LS with | nil => l | l :: _ => l end with | nil => fun _ => f | l :: ls => hlist_hd end Y) (match LS as LS return hlist LS -> hlist match LS with | nil => ls | _ :: ls => ls end with | nil => fun _ => x | l :: ls => hlist_tl end Y) with | hlist_eqv_nil => I | hlist_eqv_cons l ls x y h1 h2 pf1 pf2 => _ end IHx). simpl. subst. intros. f_equal. apply H0. assumption. } { intros; subst. constructor; auto. reflexivity. } } 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