proposition: Lemma ForallPairs_ForallOrdPairs l: ForallPairs l -> ForallOrdPairs l.
proof: Proof. induction l as [|a l IHl]; [easy|]. intros H. constructor. - rewrite Forall_forall. intros; apply H; simpl; auto. - apply IHl. red; intros; apply H; simpl; auto. Qed.
imports: PeanoNat