proposition: Theorem recurrence_axiom : forall x e, rec↓e ⊩ ℕ x.
proof: Proof. Ksolve. apply (Y_realizer lt_wf). find. Ksolve. destruct x0. fork1. Keval. apply mℕ_storage. now find. fork2. Ksolve. now apply lt_n_Sn. start. apply succℕ_realizer. replace (S x0) with (x0 + 1) in Hπ. find. ring. Qed.
imports: Arith Omega ClassicalRealizability.Kbase ClassicalRealizability.Integers ClassicalRealizability.KBool