proposition: Lemma equiv_inter_Bool : (∀A B, A → B → A) ∩ (∀A B, A → B → B) ≈ 𝔹 0 ∩ 𝔹 1.
proof: Proof. apply subtype_eqtype; apply inter_sub_compat. subtyping. subtyping. apply sub_Forall_add. intro A. apply sub_Forall_add. intro B. etransitivity. apply (sub_Forall _ (fun n : nat => if eq_nat_dec n 0 then A else B)). simpl. reflexivity. apply sub_Forall_add. intro A. apply sub_Forall_add. intro B. etransitivity. apply (sub_Forall _ (fun n : nat => if eq_nat_dec n 0 then A else B)). simpl. reflexivity. Qed.
imports: Arith Omega ClassicalRealizability.Kbase ClassicalRealizability.Integers ClassicalRealizability.KBool