@@ -0,0 +1,28 @@
6+andSameNeutral : (x : Bool) -> x && x = x
7+andSameNeutral False = Refl
8+andSameNeutral True = Refl
10+andFalseFalse : (x : Bool) -> x && False = False
11+andFalseFalse False = Refl
12+andFalseFalse True = Refl
14+andTrueNeutral : (x : Bool) -> x && True = x
15+andTrueNeutral False = Refl
16+andTrueNeutral True = Refl
18+orSameNeutral : (x : Bool) -> x || x = x
19+orSameNeutral False = Refl
20+orSameNeutral True = Refl
22+orFalseNeutral : (x : Bool) -> x || False = x
23+orFalseNeutral False = Refl
24+orFalseNeutral True = Refl
26+orTrueTrue : (x : Bool) -> x || True = True
27+orTrueTrue False = Refl
28+orTrueTrue True = Refl