proposition: Lemma ℚeq_realizer : forall e, ℚeq↓e ⊩ ∀₂p,q∈ℚ×ℚ, ∀A B, (p = q ↦ A) → (~p = q ↦ B) → (p = q ↦ A) ∩ (~p = q ↦ B).
proof: Proof. intro e. start. destruct (Qc_eq_dec p q); destruct Hπ; Ksolve; contradiction. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase