proposition: Lemma equiv_fork_rec : forall e, fork_rec↓e ⊩ (𝔹 0 ∩ 𝔹 1) → ∀x, ℕ x.
proof: Proof. Ksolve. apply (Y_realizer lt_wf). find. Ksolve. destruct x0. left. exists (fun n : nat => if eq_nat_dec n 0 then ℕ 0 else ⊤). Ksolve. Ksolve. apply mℕ_storage. exists 0. now find. simpl. ok. right. exists (fun n : nat => if eq_nat_dec n 0 then ⊤ else ℕ (S x0)). simpl. Ksolve. 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