proposition: Lemma equiv_TopBot_Bool : forall e, TopBot_Bool↓e ⊩ (⊥ → ⊤ → ⊥) ∩ (⊤ → ⊥ → ⊥) → 𝔹 0 ∩ 𝔹 1.
proof: Proof. unfold 𝔹. Ksolve. left. do 2 Ksolve. right. do 2 Ksolve. Qed.
imports: Arith Omega ClassicalRealizability.Kbase ClassicalRealizability.Integers ClassicalRealizability.KBool