proposition: Theorem hlist_hrel_map : forall ls xs ys, @hlist_hrel A F G R ls xs ys -> @hlist_hrel A F' G' R' ls (hlist_map ff xs) (hlist_map gg ys).
proof: Proof. induction 1; simpl; 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