Proposition not_not_is_regular_element {H : complete_heyting_algebra} (x : H) : ¬ ¬ x = ¬ ¬ ¬ ¬ x. Proof. use make_is_regular_element. use cha_to_le_exp. refine (cha_le_trans _ (cha_exp_eval (¬ ¬ ¬ x) _)). use cha_min_le_case. - use cha_min_le_l. - refine (cha_le_trans (cha_min_le_r _ _) _). apply cha_not_not. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.OrderTheory.Lattice.DerivedLawsCompleteHeyting.