proposition: Remark Forall2_R {A B: Type} (R: A -> B -> Prop) : forall l l', Forall2 R l l' -> Forall2R R l l'.
proof: Proof. induction 1. - constructor. - inversion IHForall2. + eright with nil nil x y;auto. now left. + subst; apply Forall2R_cons; auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)