proposition: Lemma equiv_rec_case : forall e, rec_case↓e ⊩ (∀x, ℕ x) → (∀x, x ≡ 0 ∨ ∃y, x ≡ S y).
proof: Proof. do 2 Ksolve. apply mℕ_storage. exists 0. find. start. apply ℕeq_realizer2. exists 0. exists x. find. Ksolve. Ksolve. subst. start. apply Id_realizer. destruct Hπ as [[Hc0 Hπ] | [Hc0 Hπ]]. ok. now elim Hc0. Ksolve. Kmove. exists (pred x). Kmove. start. apply Id_realizer. destruct Hπ as [[Hc0 Hπ] | [Hc0 Hπ]]. ok. elim Hc0. apply (S_pred x 0). omega. Qed.
imports: Arith Omega ClassicalRealizability.Kbase ClassicalRealizability.Integers ClassicalRealizability.KBool