proposition: Lemma equiv_hlist_map : forall T U (F : T -> Type) (R : forall t, F t -> F t -> Prop) (R' : forall t, U t -> U t -> Prop) (f g : forall t, F t -> U t), (forall t (x y : F t), R t x y -> R' t (f t x) (g t y)) -> forall ls (a b : hlist F ls), equiv_hlist R a b -> equiv_hlist R' (hlist_map f a) (hlist_map g b).
proof: Proof. clear. induction 2; simpl; intros. - constructor. - constructor; eauto. 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