fact: Axiom thm_PAIRWISE_IMPLIES : forall {A : Type'}, forall R : A -> A -> Prop, forall R' : A -> A -> Prop, forall l : list A, ((@List.ForallOrdPairs A R l) /\ (forall x : A, forall y : A, ((@List.In A x l) /\ ((@List.In A y l) /\ (R x y))) -> R' x y)) -> @List.ForallOrdPairs A R' l.
imports: coq theory_hol types terms axioms