>>126
coq8.4からη変換が入ったみたいね
多分これでη変換無しで行けると思う

Variable A:Type.
Variable B:(A -> Type) -> A -> Type.
Definition mu := fun (x:A) => forall P:(A -> Type), (forall (y:A), B P y -> P y) -> P x.
Hypothesis m : forall (P Q:A -> Type), (forall (x:A), P x -> Q x) -> (forall (x:A), B P x -> B Q x).

Theorem r1:forall (x:A), B mu x -> mu x.
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.

intros y0 c.
apply b.
apply (m (fun x : A => P x) P).
trivial.
exact c.
exact a.
Qed.