proposition: Lemma merge_lt_wf : forall P : S1 -> S2 -> Prop, (forall (q : S1) (t : S2), (forall (r : S1) (u : S2), merge_lt r u q t -> P r u) -> P q t) -> forall (x : S1) (p : S2), P x p.
proof: Proof. intros. assert (forall r : S1, (forall r' : S1, O1 r' r -> forall t' : S2, P r' t') -> forall t : S2, P r t). clear x p. intros x. intros. set (x_aux := x) in *. assert (E1 x_aux x). unfold x_aux in |- *. elim (is_eq S1). intros. apply H1. generalize H1. generalize x_aux. apply (S2ind_wf (fun p : S2 => forall x_aux : S1, E1 x_aux x -> P x_aux p)). intros. apply H. intros. case H4. intro. apply H0. apply (ord_wd_rht S1) with x_aux0. assumption. assumption. intro a. elim a. intros. apply H2. assumption. elim (is_eq S1). intros. elim H8. intros. apply H10 with x_aux0. assumption. assumption. generalize x. clear x. apply (S2ind_wf (fun p : S2 => forall x : S1, P x p)). intros. apply H. clear p. intros x' p. intro. case H2. intro. generalize p. assert (S1ind_wf_ : forall P : S1 -> Prop, (forall q : S1, (forall r : S1, O1 r q -> P r) -> P q) -> forall t : S1, P t). apply S1ind_wf. apply S1ind_wf_ with (P := fun x : S1 => forall p1 : S2, P x p1). intros. apply H0. intros. apply H4. assumption. intro a. elim a. intros. apply H1. assumption. Defined.