proposition: Remark Forall2R_cons {A B: Type} (R: A -> B -> Prop): forall l l', Forall2R R l l' -> forall x y, R x y -> Forall2R R (x::l) (y:: l').
proof: Proof. induction 1. - intros. eright with nil nil x y ; auto. left. - intros; subst; right with (x0::l) (y0::l') x y; auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)