proposition: Remark Forall2_RR {A B: Type} (R: A -> B -> Prop) : forall l l', Forall2R R l l' -> Forall2 R l l'.
proof: Proof. induction 1. - constructor. - subst; apply Forall2_app; auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)