proposition: Lemma ForallOrdPairs_inclA : forall l l', NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'.
proof: Proof. intros l l'. induction l' as [|x l' IH]. - constructor. - intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto. rewrite Forall_forall; intros y Hy. assert (Ix : InA x (x::l')) by (rewrite InA_cons; auto). apply Incl in Ix. rewrite InA_alt in Ix. destruct Ix as (x' & Hxx' & Hx'). assert (Iy : InA y (x::l')) by (apply In_InA; simpl; auto). apply Incl in Iy. rewrite InA_alt in Iy. destruct Iy as (y' & Hyy' & Hy'). rewrite Hxx', Hyy'. destruct (ForallOrdPairs_In FOP x' y' Hx' Hy') as [E|[?|?]]; auto. absurd (InA x l'); auto. rewrite Hxx', E, <- Hyy'; auto. Qed.
imports: List Sorted Setoid Basics Morphisms