content: -----------------------------------------------------------------------------
  -- |
  -- Module    : Documentation.SBV.Examples.TP.ShefferStroke
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Inspired by https://www.philipzucker.com/cody_sheffer/, proving
  -- that the axioms of sheffer stroke (i.e., nand in traditional boolean
  -- logic), imply it is a boolean algebra.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE DataKinds            #-}
  {-# LANGUAGE FlexibleInstances    #-}
  {-# LANGUAGE NamedFieldPuns       #-}
  {-# LANGUAGE ScopedTypeVariables  #-}
  {-# LANGUAGE TemplateHaskell      #-}
  {-# LANGUAGE TypeAbstractions     #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module Documentation.SBV.Examples.TP.ShefferStroke where
  
  import Prelude hiding ((<))
  import Data.List (intercalate)
  
  import Data.SBV
  import Data.SBV.TP
  
  -- * Generalized Boolean Algebras
  
  -- | Capture what it means to be a boolean algebra. We follow Lean's
  -- definition, as much as we can: <https://leanprover-community.github.io/mathlib_docs/order/boolean_algebra.html>.
  -- Since there's no way in Haskell to capture properties together with a class, we'll represent the properties
  -- separately.
  class BooleanAlgebra α where
    ﬧ    :: α -> α
    (⨆)  :: α -> α -> α
    (⨅)  :: α -> α -> α
    (≤)  :: α -> α -> SBool
    (<)  :: α -> α -> SBool
    (\\) :: α -> α -> α
    (⇨)  :: α -> α -> α
    ⲳ    :: α
    т    :: α
  
    infix  4 ≤
    infixl 6 ⨆
    infixl 7 ⨅
  
  -- | Proofs needed for a boolean-algebra. Again, we follow Lean's definition here. Since we cannot
  -- put these in the class definition above, we will keep them in a simple data-structure.
  data BooleanAlgebraProof = BooleanAlgebraProof {
      le_refl          {- ∀ (a : α), a ≤ a                             -} :: Proof (Forall "a" Stroke -> SBool)
    , le_trans         {- ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c         -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
    , lt_iff_le_not_le {- (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)        -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
    , le_antisymm      {- ∀ (a b : α), a ≤ b → b ≤ a → a = b           -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
    , le_sup_left      {- ∀ (a b : α), a ≤ a ⊔ b                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
    , le_sup_right     {- ∀ (a b : α), b ≤ a ⊔ b                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
    , sup_le           {- ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c     -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
    , inf_le_left      {- ∀ (a b : α), a ⊓ b ≤ a                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
    , inf_le_right     {- ∀ (a b : α), a ⊓ b ≤ b                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
    , le_inf           {- ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c     -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
    , le_sup_inf       {- ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
    , inf_compl_le_bot {- ∀ (x : α), x ⊓ xᶜ ≤ ⊥                        -} :: Proof (Forall "x" Stroke -> SBool)
    , top_le_sup_compl {- ∀ (x : α), ⊤ ≤ x ⊔ xᶜ                        -} :: Proof (Forall "x" Stroke -> SBool)
    , le_top           {- ∀ (a : α), a ≤ ⊤                             -} :: Proof (Forall "a" Stroke -> SBool)
    , bot_le           {- ∀ (a : α), ⊥ ≤ a                             -} :: Proof (Forall "a" Stroke -> SBool)
    , sdiff_eq         {- (∀ (x y : α), x \ y = x ⊓ yᶜ)                -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
    , himp_eq          {- (∀ (x y : α), x ⇨ y = y ⊔ xᶜ)                -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
    }
  
  -- | A somewhat prettier printer for a BooleanAlgebra proof
  instance Show BooleanAlgebraProof where
    show p = intercalate "\n" [ "BooleanAlgebraProof {"
                              , "  le_refl         : " ++ show (le_refl          p)
                              , "  le_trans        : " ++ show (le_trans         p)
                              , "  lt_iff_le_not_le: " ++ show (lt_iff_le_not_le p)
                              , "  le_antisymm     : " ++ show (le_antisymm      p)
                              , "  le_sup_left     : " ++ show (le_sup_left      p)
                              , "  le_sup_right    : " ++ show (le_sup_right     p)
                              , "  sup_le          : " ++ show (sup_le           p)
                              , "  inf_le_left     : " ++ show (inf_le_left      p)
                              , "  inf_le_right    : " ++ show (inf_le_right     p)
                              , "  le_inf          : " ++ show (le_inf           p)
                              , "  le_sup_inf      : " ++ show (le_sup_inf       p)
                              , "  inf_compl_le_bot: " ++ show (inf_compl_le_bot p)
                              , "  top_le_sup_compl: " ++ show (top_le_sup_compl p)
                              , "  le_top          : " ++ show (le_top           p)
                              , "  bot_le          : " ++ show (bot_le           p)
                              , "  sdiff_eq        : " ++ show (sdiff_eq         p)
                              , "  himp_eq         : " ++ show (himp_eq          p)
                              , "}"
                              ]
  
  -- * The sheffer stroke
  
  -- | The abstract type for the domain.
  data Stroke
  mkSymbolic [''Stroke]
  
  -- | The sheffer stroke operator.
  (⏐) :: SStroke -> SStroke -> SStroke
  (⏐) = uninterpret "⏐"
  infixl 7 ⏐
  
  -- | The boolean algebra of the sheffer stroke.
  instance BooleanAlgebra SStroke where
    ﬧ x    = x ⏐ x
    a ⨆ b  = ﬧ(a ⏐ b)
    a ⨅ b  = ﬧ a ⏐ ﬧ b
    a ≤ b  = a .== b ⨅ a
    a < b  = a ≤ b .&& a ./= b
    a \\ b = a ⨅ ﬧ b
    a ⇨ b  = b ⨆ ﬧ a
    ⲳ      = arb ⏐ ﬧ arb where arb = some "ⲳ" (const sTrue)
    т      = ﬧ ⲳ
  
  -- | Double-negation
  ﬧﬧ :: BooleanAlgebra a => a -> a
  ﬧﬧ = ﬧ . ﬧ
  
  -- | First Sheffer axiom: @ﬧﬧa == a@
  sheffer1 :: TP (Proof (Forall "a" Stroke -> SBool))
  sheffer1 = axiom "ﬧﬧa == a" $ \(Forall a) -> ﬧﬧ a .== a
  
  -- | Second Sheffer axiom: @a ⏐ (b ⏐ ﬧb) == ﬧa@
  sheffer2 :: TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
  sheffer2 = axiom "a ⏐ (b ⏐ ﬧb) == ﬧa" $ \(Forall a) (Forall b) -> a ⏐ (b ⏐ ﬧ b) .== ﬧ a
  
  -- | Third Sheffer axiom: @ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)@
  sheffer3 :: TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
  sheffer3 = axiom "ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)" $ \(Forall a) (Forall b) (Forall c) -> ﬧ(a ⏐ (b ⏐ c)) .== (ﬧ b ⏐ a) ⏐ (ﬧ c ⏐ a)
  
  -- * Sheffer's stroke defines a boolean algebra
  
  -- | Prove that Sheffer stroke axioms imply it is a boolean algebra. We have:
  --
  -- >>> shefferBooleanAlgebra
  -- Axiom: ﬧﬧa == a
  -- Axiom: a ⏐ (b ⏐ ﬧb) == ﬧa
  -- Axiom: ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)
  -- Lemma: a | b = b | a
  --   Step: 1 (ﬧﬧa == a)                                        Q.E.D.
  --   Step: 2 (ﬧﬧa == a)                                        Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4 (ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a))           Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6 (ﬧﬧa == a)                                        Q.E.D.
  --   Step: 7 (ﬧﬧa == a)                                        Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a | a′ = b | b′
  --   Step: 1 (ﬧﬧa == a)                                        Q.E.D.
  --   Step: 2 (a ⏐ (b ⏐ ﬧb) == ﬧa)                              Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4 (a ⏐ (b ⏐ ﬧb) == ﬧa)                              Q.E.D.
  --   Step: 5 (ﬧﬧa == a)                                        Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊔ b = b ⊔ a                                        Q.E.D.
  -- Lemma: a ⊓ b = b ⊓ a                                        Q.E.D.
  -- Lemma: a ⊔ ⲳ = a                                            Q.E.D.
  -- Lemma: a ⊓ т = a                                            Q.E.D.
  -- Lemma: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)                      Q.E.D.
  -- Lemma: a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)                      Q.E.D.
  -- Lemma: a ⊔ aᶜ = т                                           Q.E.D.
  -- Lemma: a ⊓ aᶜ = ⲳ                                           Q.E.D.
  -- Lemma: a ⊔ т = т
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊓ ⲳ = ⲳ
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊔ (a ⊓ b) = a
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊓ (a ⊔ b) = a
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊓ a = a
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Step: 7                                                   Q.E.D.
  --   Step: 8                                                   Q.E.D.
  --   Step: 9                                                   Q.E.D.
  --   Step: 10                                                  Q.E.D.
  --   Step: 11                                                  Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: aᶜᶜ = a                                              Q.E.D.
  -- Lemma: aᶜ = bᶜ → a = b                                      Q.E.D.
  -- Lemma: a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b                      Q.E.D.
  -- Lemma: a ⊔ (aᶜ ⊔ b) = т
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊓ (aᶜ ⊓ b) = ⲳ
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ                                   Q.E.D.
  -- Lemma: (a ⨅ b)ᶜ = aᶜ ⨆ bᶜ                                   Q.E.D.
  -- Lemma: (a ⊔ (b ⊔ c)) ⊔ aᶜ = т                               Q.E.D.
  -- Lemma: b ⊓ (a ⊔ (b ⊔ c)) = b                                Q.E.D.
  -- Lemma: b ⊔ (a ⊓ (b ⊓ c)) = b                                Q.E.D.
  -- Lemma: (a ⊔ (b ⊔ c)) ⊔ bᶜ = т
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Step: 7                                                   Q.E.D.
  --   Step: 8                                                   Q.E.D.
  --   Step: 9                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: (a ⊔ (b ⊔ c)) ⊔ cᶜ = т                               Q.E.D.
  -- Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Step: 7                                                   Q.E.D.
  --   Step: 8                                                   Q.E.D.
  --   Step: 9                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ                                 Q.E.D.
  -- Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ                                 Q.E.D.
  -- Lemma: (a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Step: 7                                                   Q.E.D.
  --   Step: 8                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: (a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Step: 5                                                   Q.E.D.
  --   Step: 6                                                   Q.E.D.
  --   Step: 7                                                   Q.E.D.
  --   Step: 8                                                   Q.E.D.
  --   Step: 9                                                   Q.E.D.
  --   Step: 10                                                  Q.E.D.
  --   Step: 11                                                  Q.E.D.
  --   Step: 12                                                  Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c                            Q.E.D.
  -- Lemma: a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ≤ b → b ≤ a → a = b
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ≤ a                                                Q.E.D.
  -- Lemma: a ≤ b → b ≤ c → a ≤ c
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Step: 4                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a < b ↔ a ≤ b ∧ ¬b ≤ a                               Q.E.D.
  -- Lemma: a ≤ a ⊔ b                                            Q.E.D.
  -- Lemma: b ≤ a ⊔ b                                            Q.E.D.
  -- Lemma: a ≤ c → b ≤ c → a ⊔ b ≤ c
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: a ⊓ b ≤ a                                            Q.E.D.
  -- Lemma: a ⊓ b ≤ b                                            Q.E.D.
  -- Lemma: a ≤ b → a ≤ c → a ≤ b ⊓ c
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z                        Q.E.D.
  -- Lemma: x ⊓ xᶜ ≤ ⊥                                           Q.E.D.
  -- Lemma: ⊤ ≤ x ⊔ xᶜ                                           Q.E.D.
  -- Lemma: a ≤ ⊤
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Step: 3                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: ⊥ ≤ a
  --   Step: 1                                                   Q.E.D.
  --   Step: 2                                                   Q.E.D.
  --   Result:                                                   Q.E.D.
  -- Lemma: x \ y = x ⊓ yᶜ                                       Q.E.D.
  -- Lemma: x ⇨ y = y ⊔ xᶜ                                       Q.E.D.
  -- BooleanAlgebraProof {
  --   le_refl         : [Proven] a ≤ a :: Ɐa ∷ Stroke → Bool
  --   le_trans        : [Proven] a ≤ b → b ≤ c → a ≤ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
  --   lt_iff_le_not_le: [Proven] a < b ↔ a ≤ b ∧ ¬b ≤ a :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
  --   le_antisymm     : [Proven] a ≤ b → b ≤ a → a = b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
  --   le_sup_left     : [Proven] a ≤ a ⊔ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
  --   le_sup_right    : [Proven] b ≤ a ⊔ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
  --   sup_le          : [Proven] a ≤ c → b ≤ c → a ⊔ b ≤ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
  --   inf_le_left     : [Proven] a ⊓ b ≤ a :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
  --   inf_le_right    : [Proven] a ⊓ b ≤ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
  --   le_inf          : [Proven] a ≤ b → a ≤ c → a ≤ b ⊓ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
  --   le_sup_inf      : [Proven] (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Ɐz ∷ Stroke → Bool
  --   inf_compl_le_bot: [Proven] x ⊓ xᶜ ≤ ⊥ :: Ɐx ∷ Stroke → Bool
  --   top_le_sup_compl: [Proven] ⊤ ≤ x ⊔ xᶜ :: Ɐx ∷ Stroke → Bool
  --   le_top          : [Proven] a ≤ ⊤ :: Ɐa ∷ Stroke → Bool
  --   bot_le          : [Proven] ⊥ ≤ a :: Ɐa ∷ Stroke → Bool
  --   sdiff_eq        : [Proven] x \ y = x ⊓ yᶜ :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Bool
  --   himp_eq         : [Proven] x ⇨ y = y ⊔ xᶜ :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Bool
  -- }
  shefferBooleanAlgebra :: IO BooleanAlgebraProof
  shefferBooleanAlgebra = runTPWith (tpRibbon 60 z3) $ do
  
    -- shorthand
    let p = proofOf
  
    -- Get the axioms
    sh1 <- sheffer1
    sh2 <- sheffer2
    sh3 <- sheffer3
  
    commut <- calc "a | b = b | a" (\(Forall @"a" a) (Forall @"b" b) -> a ⏐ b .== b ⏐ a) $
                   \a b -> [] ⊢ a ⏐ b                       ∵ sh1
                              ≡ ﬧﬧ(a ⏐ b)                   ∵ sh1
                              ≡ ﬧﬧ(a ⏐ ﬧﬧ b)
                              ≡ ﬧﬧ(a ⏐ (ﬧ b ⏐ ﬧ b))         ∵ sh3
                              ≡ ﬧ ((ﬧﬧ b ⏐ a) ⏐ (ﬧﬧ b ⏐ a))
                              ≡ ﬧﬧ(ﬧﬧ b ⏐ a)                ∵ sh1
                              ≡ ﬧﬧ b ⏐ a                    ∵ sh1
                              ≡ b ⏐ a
                              ≡ qed
  
    all_bot <- calc "a | a′ = b | b′" (\(Forall @"a" a) (Forall @"b" b) -> a ⏐ ﬧ a .== b ⏐ ﬧ b) $
                    \a b -> [] ⊢ a ⏐ ﬧ a                  ∵ sh1
                               ≡ ﬧﬧ(a ⏐ ﬧ a)              ∵ sh2
                               ≡ ﬧ((a ⏐ ﬧ a) ⏐ (b ⏐ ﬧ b)) ∵ commut
                               ≡ ﬧ((b ⏐ ﬧ b) ⏐ (a ⏐ ﬧ a)) ∵ sh2
                               ≡ ﬧﬧ (b ⏐ ﬧ b)             ∵ sh1
                               ≡ b ⏐ ﬧ b
                               ≡ qed
  
    commut1  <- lemma "a ⊔ b = b ⊔ a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨆ b .== b ⨆ a) [p commut]
    commut2  <- lemma "a ⊓ b = b ⊓ a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ b .== b ⨅ a) [p commut]
  
    ident1   <- lemma "a ⊔ ⲳ = a" (\(Forall @"a" (a :: SStroke)) -> a ⨆ ⲳ .== a) [p sh1, p sh2]
    ident2   <- lemma "a ⊓ т = a" (\(Forall @"a" (a :: SStroke)) -> a ⨅ т .== a) [p sh1, p sh2]
  
    distrib1 <- lemma "a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)"
                      (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨆ (b ⨅ c) .== (a ⨆ b) ⨅ (a ⨆ c))
                      [p sh1, p sh3, p commut]
  
    distrib2 <- lemma "a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)"
                      (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨅ (b ⨆ c) .== (a ⨅ b) ⨆ (a ⨅ c))
                      [p sh1, p sh3, p commut]
  
    compl1 <- lemma "a ⊔ aᶜ = т" (\(Forall @"a" (a :: SStroke)) -> a ⨆ ﬧ a .== т) [p sh1, p sh2, p sh3, p all_bot]
    compl2 <- lemma "a ⊓ aᶜ = ⲳ" (\(Forall @"a" (a :: SStroke)) -> a ⨅ ﬧ a .== ⲳ) [p sh1, p commut, p all_bot]
  
    bound1 <- calc "a ⊔ т = т" (\(Forall @"a"  a) -> a ⨆ т .== т) $
                   \a -> [] ⊢ a ⨆ т               ∵ ident2
                             ≡ (a ⨆ т) ⨅ т         ∵ commut2
                             ≡ т ⨅ (a ⨆ т)         ∵ compl1
                             ≡ (a ⨆ ﬧ a) ⨅ (a ⨆ т) ∵ distrib1
                             ≡ a ⨆ (ﬧ a ⨅ т)       ∵ ident2
                             ≡ a ⨆ ﬧ a             ∵ compl1
                             ≡ (т :: SStroke)
                             ≡ qed
  
    bound2 <- calc "a ⊓ ⲳ = ⲳ" (\(Forall @"a" a) -> a ⨅ ⲳ .== ⲳ) $
                   \a -> [] ⊢ a ⨅ ⲳ               ∵ ident1
                             ≡ (a ⨅ ⲳ) ⨆ ⲳ         ∵ commut1
                             ≡ ⲳ ⨆ (a ⨅ ⲳ)         ∵ compl2
                             ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ ⲳ) ∵ distrib2
                             ≡ a ⨅ (ﬧ a ⨆ ⲳ)       ∵ ident1
                             ≡ a ⨅ ﬧ a             ∵ compl2
                             ≡ (ⲳ :: SStroke)
                             ≡ qed
  
    absorb1 <- calc "a ⊔ (a ⊓ b) = a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨆ (a ⨅ b) .== a) $
                    \a b -> [] ⊢ a ⨆ (a ⨅ b)       ∵ ident2
                               ≡ (a ⨅ т) ⨆ (a ⨅ b) ∵ distrib2
                               ≡ a ⨅ (т ⨆ b)       ∵ commut1
                               ≡ a ⨅ (b ⨆ т)       ∵ bound1
                               ≡ a ⨅ т             ∵ ident2
                               ≡ a
                               ≡ qed
  
    absorb2 <- calc "a ⊓ (a ⊔ b) = a" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ (a ⨆ b) .== a) $
                    \a b -> [] ⊢ a ⨅ (a ⨆ b)       ∵ ident1
                               ≡ (a ⨆ ⲳ) ⨅ (a ⨆ b) ∵ distrib1
                               ≡ a ⨆ (ⲳ ⨅ b)       ∵ commut2
                               ≡ a ⨆ (b ⨅ ⲳ)       ∵ bound2
                               ≡ a ⨆ ⲳ             ∵ ident1
                               ≡ a
                               ≡ qed
  
    idemp2 <- calc "a ⊓ a = a" (\(Forall @"a" (a :: SStroke)) -> a ⨅ a .== a) $
                   \a -> [] ⊢ a ⨅ a       ∵ ident1
                            ≡ a ⨅ (a ⨆ ⲳ) ∵ absorb2
                            ≡ a
                            ≡ qed
  
    inv <- calc "a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ"
                (\(Forall @"a" (a :: SStroke)) (Forall @"a'" a') -> a ⨆ a' .== т .=> a ⨅ a' .== ⲳ .=> a' .== ﬧ a) $
                \a a' -> [a ⨆ a' .== т, a ⨅ a' .== ⲳ] ⊢ a'                     ∵ ident2
                                                      ≡ a' ⨅ т                 ∵ compl1
                                                      ≡ a' ⨅ (a ⨆ ﬧ a)         ∵ distrib2
                                                      ≡ (a' ⨅ a) ⨆ (a' ⨅ ﬧ a)  ∵ commut2
                                                      ≡ (a' ⨅ a) ⨆ (ﬧ a ⨅ a')  ∵ commut2
                                                      ≡ (a ⨅ a') ⨆ (ﬧ a ⨅ a')  ∵ a ⨅ a' .== ⲳ
                                                      ≡ ⲳ ⨆ (ﬧ a ⨅ a')         ∵ compl2
                                                      ≡ (a ⨅ ﬧ a) ⨆ (ﬧ a ⨅ a') ∵ commut2
                                                      ≡ (ﬧ a ⨅ a) ⨆ (ﬧ a ⨅ a') ∵ distrib2
                                                      ≡ ﬧ a ⨅ (a ⨆ a')         ∵ a ⨆ a' .== т
                                                      ≡ ﬧ a ⨅ т                ∵ ident2
                                                      ≡ ﬧ a
                                                      ≡ qed
  
    dne      <- lemma "aᶜᶜ = a"
                      (\(Forall @"a" (a :: SStroke)) -> ﬧﬧ a .== a)
                      [p inv, p compl1, p compl2, p commut1, p commut2]
  
    inv_elim <- lemma "aᶜ = bᶜ → a = b"
                      (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> ﬧ a .== ﬧ b .=> a .== b)
                      [p dne]
  
    cancel <- lemma "a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b"
                    (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨆ ﬧ b .== т .=> a ⨅ ﬧ b .== ⲳ .=> a .== b)
                    [p inv, p inv_elim]
  
    a1 <- calc "a ⊔ (aᶜ ⊔ b) = т" (\(Forall @"a" a) (Forall @"b" b)  -> a ⨆ (ﬧ a ⨆ b) .== т) $
               \a b -> [] ⊢ a ⨆ (ﬧ a ⨆ b)               ∵ ident2
                          ≡ (a ⨆ (ﬧ a ⨆ b)) ⨅ т         ∵ commut2
                          ≡ т ⨅ (a ⨆ (ﬧ a ⨆ b))         ∵ compl1
                          ≡ (a ⨆ ﬧ a) ⨅ (a ⨆ (ﬧ a ⨆ b)) ∵ distrib1
                          ≡ a ⨆ (ﬧ a ⨅ (ﬧ a ⨆ b))       ∵ absorb2
                          ≡ a ⨆ ﬧ a                     ∵ compl1
                          ≡ (т :: SStroke)
                          ≡ qed
  
    a2 <- calc "a ⊓ (aᶜ ⊓ b) = ⲳ" (\(Forall @"a" a) (Forall @"b" b)  -> a ⨅ (ﬧ a ⨅ b) .== ⲳ) $
               \a b -> [] ⊢ a ⨅ (ﬧ a ⨅ b)               ∵ ident1
                          ≡ (a ⨅ (ﬧ a ⨅ b)) ⨆ ⲳ         ∵ commut1
                          ≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ b))         ∵ compl2
                          ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ b)) ∵ distrib2
                          ≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ b))       ∵ absorb1
                          ≡ a ⨅ ﬧ a                     ∵ compl2
                          ≡ (ⲳ :: SStroke)
                          ≡ qed
  
    dm1 <- lemma "(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ"
                 (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> ﬧ(a ⨆ b) .== ﬧ a ⨅ ﬧ b)
                 [p a1, p a2, p dne, p commut1, p commut2, p ident1, p ident2, p distrib1, p distrib2]
  
    dm2 <- lemma "(a ⨅ b)ᶜ = aᶜ ⨆ bᶜ"
                 (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> ﬧ(a ⨅ b) .== ﬧ a ⨆ ﬧ b)
                 [p a1, p a2, p dne, p commut1, p commut2, p ident1, p ident2, p distrib1, p distrib2]
  
  
    d1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ aᶜ = т"
                (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ a .== т)
                [p a1, p a2, p commut1, p ident1, p ident2, p distrib1, p compl1, p compl2, p dm1, p dm2, p idemp2]
  
    e1 <- lemma "b ⊓ (a ⊔ (b ⊔ c)) = b"
                (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> b ⨅ (a ⨆ (b ⨆ c)) .== b)
                [p distrib2, p absorb1, p absorb2, p commut1]
  
    e2 <- lemma "b ⊔ (a ⊓ (b ⊓ c)) = b" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> b ⨆ (a ⨅ (b ⨅ c)) .== b) [p distrib1, p absorb1, p absorb2, p commut2]
  
    f1 <- calc "(a ⊔ (b ⊔ c)) ⊔ bᶜ = т" (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ b .== т) $
               \a b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ b               ∵ commut1
                            ≡ ﬧ b ⨆ (a ⨆ (b ⨆ c))               ∵ ident2
                            ≡ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ⨅ т         ∵ commut2
                            ≡ т ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c)))         ∵ compl1
                            ≡ (b ⨆ ﬧ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ∵ commut1
                            ≡ (ﬧ b ⨆ b) ⨅ (ﬧ b ⨆ (a ⨆ (b ⨆ c))) ∵ distrib1
                            ≡ ﬧ b ⨆ (b ⨅ (a ⨆ (b ⨆ c)))         ∵ e1
                            ≡ ﬧ b ⨆ b                           ∵ commut1
                            ≡ b ⨆ ﬧ b                           ∵ compl1
                            ≡ (т :: SStroke)
                            ≡ qed
  
    g1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ cᶜ = т"
                (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ c .== т)
                [p commut1, p f1]
  
    h1 <- calc "(a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ"
               (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> ﬧ(a ⨆ b ⨆ c) ⨅ a .== ⲳ) $
               \a b c -> [] ⊢ ﬧ(a ⨆ b ⨆ c) ⨅ a                    ∵ commut2
                            ≡ a ⨅ ﬧ (a ⨆ b ⨆ c)                   ∵ dm1
                            ≡ a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)               ∵ ident1
                            ≡ (a ⨅  (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ⨆ ⲳ        ∵ commut1
                            ≡ ⲳ ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c))         ∵ compl2
                            ≡ (a ⨅ ﬧ a) ⨆ (a ⨅ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)) ∵ distrib2
                            ≡ a ⨅ (ﬧ a ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c))       ∵ commut2
                            ≡ a ⨅ (ﬧ a ⨆ (ﬧ c ⨅ (ﬧ a ⨅ ﬧ b)))     ∵ e2
                            ≡ a ⨅ ﬧ a                             ∵ compl2
                            ≡ (ⲳ :: SStroke)
                            ≡ qed
  
    i1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ"
                (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> ﬧ(a ⨆ b ⨆ c) ⨅ b .== ⲳ)
                [p commut1, p h1]
  
    j1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ"
                (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> ﬧ(a ⨆ b ⨆ c) ⨅ c .== ⲳ)
                [p a2, p dne, p commut2]
  
  
    assoc1 <- do
      c1 <- calc "(a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т"
                 (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) .== т) $
                 \a b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c)                        ∵ dm1
                              ≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b ⨅ ﬧ c)                     ∵ distrib1
                              ≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ c) ∵ g1
                              ≡ ((a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)) ⨅ т                     ∵ ident2
                              ≡ (a ⨆ (b ⨆ c)) ⨆ (ﬧ a ⨅ ﬧ b)                           ∵ distrib1
                              ≡ ((a ⨆ (b ⨆ c)) ⨆ ﬧ a) ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b)         ∵ d1
                              ≡ т ⨅ ((a ⨆ (b ⨆ c)) ⨆ ﬧ b)                             ∵ f1
                              ≡ (т ⨅ т :: SStroke)                                    ∵ idemp2
                              ≡ (т :: SStroke)
                              ≡ qed
  
      c2 <- calc "(a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ"
                 (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) .== ⲳ) $
                 \a b c -> [] ⊢ (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c)                    ∵ commut2
                              ≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (a ⨆ (b ⨆ c))                    ∵ distrib2
                              ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c)) ∵ commut2
                              ≡ (a ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ∵ commut2
                              ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ a) ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ∵ h1
                              ≡ ⲳ ⨆ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c))                    ∵ commut1
                              ≡ ((b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)) ⨆ ⲳ                    ∵ ident1
                              ≡ (b ⨆ c) ⨅ ﬧ((a ⨆ b) ⨆ c)                          ∵ commut2
                              ≡ ﬧ((a ⨆ b) ⨆ c) ⨅ (b ⨆ c)                          ∵ distrib2
                              ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ (ﬧ((a ⨆ b) ⨆ c) ⨅ c)       ∵ j1
                              ≡ (ﬧ((a ⨆ b) ⨆ c) ⨅ b) ⨆ ⲳ                          ∵ i1
                              ≡ (ⲳ ⨆ ⲳ :: SStroke)                                ∵ ident1
                              ≡ (ⲳ :: SStroke)
                              ≡ qed
  
      lemma "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c"
            (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨆ (b ⨆ c) .== (a ⨆ b) ⨆ c)
            [p c1, p c2, p cancel]
  
    assoc2 <- calc "a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c"
                   (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) (Forall @"c" c) -> a ⨅ (b ⨅ c) .== (a ⨅ b) ⨅ c) $
                   \a b c -> [] ⊢ a ⨅ (b ⨅ c)     ∵ dne
                                ≡ ﬧﬧ(a ⨅ (b ⨅ c)) ∵ assoc1
                                ≡ ﬧﬧ((a ⨅ b) ⨅ c) ∵ dne
                                ≡   ((a ⨅ b) ⨅ c)
                                ≡ qed
  
    le_antisymm <- calc "a ≤ b → b ≤ a → a = b"
                        (\(Forall @"a" a) (Forall @"b" b) -> a ≤ b .=> b ≤ a .=> a .== b) $
                        \a b -> [a ≤ b, b ≤ a] ⊢ a     ∵ a ≤ b
                                               ≡ b ⨅ a ∵ commut2
                                               ≡ a ⨅ b ∵ b ≤ a
                                               ≡ b
                                               ≡ qed
  
    le_refl <- lemma "a ≤ a" (\(Forall @"a" a) -> a ≤ a) [p idemp2]
  
    le_trans <- calc "a ≤ b → b ≤ c → a ≤ c" (\(Forall a) (Forall b) (Forall c) -> a ≤ b .=> b ≤ c .=> a ≤ c) $
                     \a b c -> [a ≤ b, b ≤ c] ⊢ a            ∵ a ≤ b
                                              ≡ b ⨅ a        ∵ b ≤ c
                                              ≡ (c ⨅ b) ⨅ a  ∵ assoc2
                                              ≡ c ⨅ (b ⨅ a)  ∵ a ≤ b
                                              ≡ (c ⨅ a)
                                              ≡ qed
  
    lt_iff_le_not_le <- lemma "a < b ↔ a ≤ b ∧ ¬b ≤ a"
                              (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> (a < b) .<=> a ≤ b .&& sNot (b ≤ a))
                              [p sh3]
  
    le_sup_left  <- lemma "a ≤ a ⊔ b"
                    (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ≤ a ⨆ b)
                    [p commut1, p commut2, p absorb2]
  
    le_sup_right <- lemma "b ≤ a ⊔ b"
                    (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ≤ a ⨆ b)
                    [p commut1, p commut2, p absorb2]
  
    sup_le <- calc "a ≤ c → b ≤ c → a ⊔ b ≤ c"
                   (\(Forall a) (Forall b) (Forall c) -> a ≤ c .=> b ≤ c .=> a ⨆ b ≤ c) $
                   \a b c -> [a ≤ c, b ≤ c] ⊢ a ⨆ b             ∵ [a ≤ c, b ≤ c]
                                            ≡ (c ⨅ a) ⨆ (c ⨅ b) ∵ distrib2
                                            ≡ c ⨅ (a ⨆ b)
                                            ≡ qed
  
    inf_le_left  <- lemma "a ⊓ b ≤ a"
                          (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ b ≤ a)
                          [p assoc2,  p idemp2]
  
    inf_le_right <- lemma "a ⊓ b ≤ b"
                          (\(Forall @"a" (a :: SStroke)) (Forall @"b" b) -> a ⨅ b ≤ b)
                          [p commut2, p inf_le_left]
  
    le_inf <- calc "a ≤ b → a ≤ c → a ≤ b ⊓ c"
                   (\(Forall a) (Forall b) (Forall c) -> a ≤ b .=> a ≤ c .=> a ≤ b ⨅ c) $
                   \a b c -> [a ≤ b, a ≤ c] ⊢ a           ∵ a ≤ b
                                            ≡ b ⨅ a       ∵ a ≤ c
                                            ≡ b ⨅ (c ⨅ a) ∵ assoc2
                                            ≡ (b ⨅ c ⨅ a)
                                            ≡ qed
  
    le_sup_inf <- lemma "(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z"
                        (\(Forall x) (Forall y) (Forall z) -> (x ⨆ y) ⨅ (x ⨆ z) ≤ x ⨆ y ⨅ z)
                        [p distrib1, p le_refl]
  
    inf_compl_le_bot <- lemma "x ⊓ xᶜ ≤ ⊥" (\(Forall x) -> x ⨅ ﬧ x ≤ ⲳ) [p compl2, p le_refl]
    top_le_sup_compl <- lemma "⊤ ≤ x ⊔ xᶜ" (\(Forall x) -> т ≤ x ⨆ ﬧ x) [p compl1, p le_refl]
  
    le_top <- calc "a ≤ ⊤" (\(Forall @"a" a) -> a ≤ т) $
                   \a -> [] ⊢ a ≤ т
                            ≡ a .== т ⨅ a ∵ commut2
                            ≡ a .== a ⨅ т ∵ ident2
                            ≡ a .== a
                            ≡ qed
  
    bot_le <- calc "⊥ ≤ a" (\(Forall @"a" a) -> ⲳ ≤ a) $
                   \a -> [] ⊢ ⲳ ≤ a
                            ≡ ⲳ .== a ⨅ ⲳ            ∵ bound2
                            ≡ ⲳ .== (ⲳ :: SStroke)
                            ≡ qed
  
    sdiff_eq <- lemma "x \\ y = x ⊓ yᶜ" (\(Forall x) (Forall y) -> x \\ y .== x ⨅ ﬧ y) []
    himp_eq  <- lemma "x ⇨ y = y ⊔ xᶜ"  (\(Forall x) (Forall y) -> x ⇨ y .== y ⨆ ﬧ x)  []
  
    pure BooleanAlgebraProof {
              le_refl          {- ∀ (a : α), a ≤ a                             -} = le_refl
            , le_trans         {- ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c         -} = le_trans
            , lt_iff_le_not_le {- (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)        -} = lt_iff_le_not_le
            , le_antisymm      {- ∀ (a b : α), a ≤ b → b ≤ a → a = b           -} = le_antisymm
            , le_sup_left      {- ∀ (a b : α), a ≤ a ⊔ b                       -} = le_sup_left
            , le_sup_right     {- ∀ (a b : α), b ≤ a ⊔ b                       -} = le_sup_right
            , sup_le           {- ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c     -} = sup_le
            , inf_le_left      {- ∀ (a b : α), a ⊓ b ≤ a                       -} = inf_le_left
            , inf_le_right     {- ∀ (a b : α), a ⊓ b ≤ b                       -} = inf_le_right
            , le_inf           {- ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c     -} = le_inf
            , le_sup_inf       {- ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z -} = le_sup_inf
            , inf_compl_le_bot {- ∀ (x : α), x ⊓ xᶜ ≤ ⊥                        -} = inf_compl_le_bot
            , top_le_sup_compl {- ∀ (x : α), ⊤ ≤ x ⊔ xᶜ                        -} = top_le_sup_compl
            , le_top           {- ∀ (a : α), a ≤ ⊤                             -} = le_top
            , bot_le           {- ∀ (a : α), ⊥ ≤ a                             -} = bot_le
            , sdiff_eq         {- (∀ (x y : α), x \ y = x ⊓ yᶜ)                -} = sdiff_eq
            , himp_eq          {- (∀ (x y : α), x ⇨ y = y ⊔ xᶜ)                -} = himp_eq
         }
  