proposition: Theorem hlist_hrel_flip : forall T (F G : T -> Type) (R : forall t, F t -> G t -> Prop) ls (h : hlist F ls) (h' : hlist G ls), hlist_hrel R h h' -> hlist_hrel (fun t a b => R t b a) h' h.
proof: Proof. induction 1; 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