fixed true, if def, xor and thm

prelude/cert_f/booleans.lp

 require open encodings.cert_f
 
-definition bool ≔ Prop
-definition false ≔ @prod Type Prop uProp (λ x : Term uProp, x)
-definition true ≔ Term false ⇒ Term false
+definition bool ≔ uProp
+definition false ≔ @prod Type Prop uProp (λ x, x)
+definition true ≔ @prod Prop Prop false (λ _, false)
 
 definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)

prelude/cert_f/if_def.lp

+require open encodings.cert_f prelude.cert_f.booleans
+
+symbol if {T: Term uType} : Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
+
+rule if true &t  _ → &t
+ and if false _ &f → &f

prelude/cert_f/xor_def.lp

+require open encodings.cert_f prelude.cert_f.booleans prelude.cert_f.equalities
+prelude.cert_f.notequal prelude.cert_f.if_def
+
+// FIXME explicitness required
+definition xor (a b: Univ Prop) ≔ @neq uProp a b
+
+type ∀ (a b: Univ Prop), Term (xor a b)
+
+type λ (a: Term uProp), @if uProp a a a
+type ∀ a : Term uProp, Term (@if uProp a a a)
+
+// FIXME explicitness required
+theorem xor_def: ∀ (a b: Univ Prop),
+  Term (@eq uProp (xor a b) (@if uProp a (bnot b) b))
+proof
+assume a b
+simpl
+admit