@@ -0,0 +1,28 @@
1+module Data.Bool.Extra
2+
3+%access public export
4+%default total
5+
6+andSameNeutral : (x : Bool) -> x && x = x
7+andSameNeutral False = Refl
8+andSameNeutral True = Refl
9+
10+andFalseFalse : (x : Bool) -> x && False = False
11+andFalseFalse False = Refl
12+andFalseFalse True = Refl
13+
14+andTrueNeutral : (x : Bool) -> x && True = x
15+andTrueNeutral False = Refl
16+andTrueNeutral True = Refl
17+
18+orSameNeutral : (x : Bool) -> x || x = x
19+orSameNeutral False = Refl
20+orSameNeutral True = Refl
21+
22+orFalseNeutral : (x : Bool) -> x || False = x
23+orFalseNeutral False = Refl
24+orFalseNeutral True = Refl
25+
26+orTrueTrue : (x : Bool) -> x || True = True
27+orTrueTrue False = Refl
28+orTrueTrue True = Refl