proposition: Lemma prop_root : forall (P : E -> Prop) (x : E), P x -> (forall y z : E, P y -> R z y -> P z) -> P (root x).
proof: Proof. intros; generalize H. elim (wf_R x). intros; unfold root in |- *; rewrite root_eq. unfold F at 1 in |- *; case (R_dec x0); intros. elim s; intros x1 y. apply (H2 x1 y). apply H0 with (y := x0); trivial. trivial. Qed.
imports: Arith Omega List