proposition: Theorem WRA_realizer : forall e, WRA↓e ⊩ ∀P, (∀x, x == 0 → P x) → (∀y, P y → P (S y)) → ∀x, P x.
proof: Proof. Ksolve. apply Y_wra. do 2 Ksolve. Ksolve. destruct (Peano_dec.eq_nat_dec (S y) x0) as [Heq | Heq]. Ksolve. destruct (Peano_dec.eq_nat_dec x0 (S y)) as [Heq2 | Heq2]. subst. now elim Heq. ok. destruct (Peano_dec.eq_nat_dec x0 (S y)). now subst. ok. Qed.
imports: ClassicalRealizability.Kbase