ι : Type ?u.45477
α : Type u_1
β : Type ?u.45483
π : ι → Type ?u.45488
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
ι : Type ?u.45477
α : Type u_1
β : Type ?u.45483
π : ι → Type ?u.45488
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⊔ b ⇨ a ⇔ b = a ⇔ b
rw [himp_bihimp]
no goals
ι : Type ?u.45477
α : Type u_1
β : Type ?u.45483
π : ι → Type ?u.45488
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
simp [bihimp]