open import NeilPrelude1

module BoolProps1 where


∨assoc : {b c : Bool}  (a : Bool)  (a  b)  c  a  b  c
∨assoc false = refl
∨assoc true = refl

∨comm : {b : Bool}  (a : Bool)  a  b  b  a
∨comm {false} false = refl
∨comm {true} false = refl
∨comm {false} true = refl
∨comm {true} true = refl

∨idem : {b : Bool}  b  b  b
∨idem {false} = refl
∨idem {true} = refl

∨split : {a b : Bool}  a  b  false  a  false × b  false
∨split {false} eq = refl & eq
∨split {true} ()

∧assoc : {b c : Bool}  (a : Bool)  (a  b)  c  a  b  c
∧assoc false = refl
∧assoc true = refl

∧comm : {b : Bool}  (a : Bool)  a  b  b  a
∧comm {false} false = refl
∧comm {true} false = refl
∧comm {false} true = refl
∧comm {true} true = refl 

∧idem : {b : Bool}  b  b  b
∧idem {false} = refl
∧idem {true} = refl

∧split : {a b : Bool}  a  b  true  a  true × b  true
∧split {false} ()
∧split {true} eq = refl & eq

∧∨distr : {b c : Bool}  (a : Bool)  a  (b  c)  a  b  a  c
∧∨distr false = refl
∧∨distr true = refl

{-
import CommSemiRing
open module CommSR = CommSemiRing _∨_ ∨assoc ∨comm false refl _∧_ ∧assoc ∧comm refl true refl ∧∨distr public
-}