proposition: Lemma Forall2R_iff {A B: Type} (R: A -> B -> Prop) : forall l l', Forall2R R l l' <-> Forall2 R l l'.
proof: Proof. split. - intro;now apply Forall2_RR . - intro;now apply Forall2_R . Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)