proposition: Theorem hlist_hrel_cons : forall l ls x xs y ys, @hlist_hrel A F G R (l :: ls) (Hcons x xs) (Hcons y ys) -> @R l x y /\ @hlist_hrel A F G R ls xs ys.
proof: Proof. intros. refine match H in @hlist_hrel _ _ _ _ ls' xs' ys' return match ls' as ls' return hlist F ls' -> hlist G ls' -> Prop with | nil => fun _ _ => True | l' :: ls' => fun x y => R (hlist_hd x) (hlist_hd y) /\ hlist_hrel R (hlist_tl x) (hlist_tl y) end xs' ys' with | hrel_Hnil => I | hrel_Hcons _ _ _ _ _ _ pf pf' => conj pf pf' end. 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