proposition: Lemma root_no_R : forall x y : E, ~ R y (root x).
proof: Proof. intros; elim (wf_R x). intros; rewrite root_eq. unfold F at 1 in |- *; case (R_dec x0); intros. elim s; intros. fold (root x1) in |- *; apply H0; trivial. trivial. Qed.
imports: Arith Omega List