no goals
α : Type u
β : Type ?u.39786
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]