proposition: Theorem Y_realizer T (R : T -> T -> Prop) (Hwf : well_founded R) : forall e, Y↓e ⊩ ∀P, (∀x, (∀y, R y x ↦ P y) → P x) → ∀z, P z.
proof: Proof. intro e. start. revert z π Hπ. induction z as [z Hrec] using (well_founded_ind Hwf); intros. apply Ht. find. start. eapply Hrec; eok. Qed.
imports: ClassicalRealizability.Tactics