proposition: Lemma ForallOrdPairs_ForallPairs : (forall x, R x x) -> (forall x y, R x y -> R y x) -> forall l, ForallOrdPairs l -> ForallPairs l.
proof: Proof. intros Refl Sym l Hl x y Hx Hy. destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition. Qed.
imports: PeanoNat