proposition: Lemma Forall2_indR {A B : Type} (R : A -> B -> Prop) (P : list A -> list B -> Prop): P nil nil -> (forall (l : list A) (l' : list B) (x : A) (y : B) (l1 : list A) (l'1 : list B), Forall2 R l l' -> P l l' -> R x y -> l1 = l ++ x :: nil -> l'1 = l' ++ y :: nil -> P l1 l'1) -> forall (l : list A) (l0 : list B), Forall2 R l l0 -> P l l0.
proof: Proof. intros; rewrite <- Forall2R_iff in H1. eapply Forall2R_ind; eauto. intros; subst. eapply H0 with l1 l' x y; auto. now rewrite <- Forall2R_iff . Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)