proposition: Lemma ℕeq_realizer : forall e, ℤeq↓e ⊩ ∀₂n,m∈ℕ×ℕ, ∀A B, (n = m ↦ A) → (~n = m ↦ B) → (n = m ↦ A) ∩ (~n = m ↦ B).
proof: Proof. intro e. start. destruct Hπ; destruct (Z.eq_dec (Z.of_nat n) (Z.of_nat m)); rewrite Nat2Z.inj_iff in *; Ksolve; contradiction. Qed.
imports: ZArith ClassicalRealizability.Kbase