proposition: Lemma F_eq : forall (x : E) (f1 f2 : forall y : E, R y x -> E), (forall (y : E) (r : R y x), f1 y r = f2 y r) -> F x f1 = F x f2.
proof: Proof. intros; unfold F in |- *; case (R_dec x); intros. elim s; intros; auto. trivial. Qed.
imports: Arith Omega List