proposition: Lemma ForallOrdPairs_In : forall l, ForallOrdPairs l -> forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x.
proof: Proof. induction 1. - inversion 1. - simpl; destruct 1; destruct 1; subst; auto. + right; left. apply -> Forall_forall; eauto. + right; right. apply -> Forall_forall; eauto. Qed.
imports: PeanoNat