Proposition cha_min_assoc {H : complete_heyting_algebra} (x y z : H) : ((x ∧ y) ∧ z) = (x ∧ (y ∧ z)). Proof. exact (isassoc_Lmin H x y z). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting.