include "Universes.ma". ninductive Bool: Type[0] ≝ true: Bool | false: Bool. nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝ match b with [ true ⇒ t | false ⇒ f ]. notation "hvbox('if' b 'then' t 'else' f)" non associative with precedence 83 for @{ 'if_then_else $b $t $f }. interpretation "If_then_else" 'if_then_else b t f = (if_then_else ? b t f). ndefinition conjunction ≝ λb, c: Bool. match b with [ true ⇒ c | false ⇒ false ]. nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝ match b with [ true ⇒ true | false ⇒ c ]. nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝ match b with [ true ⇒ match c with [ false ⇒ true | true ⇒ false ] | false ⇒ match c with [ false ⇒ false | true ⇒ true ] ]. interpretation "Bool" 'or a b = (inclusive_disjunction a b). nlet rec negation (b: Bool) on b ≝ match b with [ true ⇒ false | false ⇒ true ].