ι : Type ?u.30631
α : Type u_1
β : Type ?u.30637
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ c ⊓ (b ⊓ a) ≤ c
ι : Type ?u.30631
α : Type u_1
β : Type ?u.30637
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]
no goals
ι : Type ?u.30631
α : Type u_1
β : Type ?u.30637
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ c ⊓ (b ⊓ a) ≤ c
exact inf_le_left