proposition: Lemma equiv_hlist_gen : forall T (F : T -> Type) (f : forall t, F t) f' (R : forall t, F t -> F t -> Prop), (forall t, R t (f t) (f' t)) -> forall ls, equiv_hlist R (hlist_gen f ls) (hlist_gen f' ls).
proof: Proof. induction ls; simpl; 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