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 (Z.eq_dec n m); Ksolve; contradiction. Qed.
imports: ZArith ClassicalRealizability.Kbase