more implicits

adlib/cert_f/booleans.lp

 require open encodings.cert_f
 
 definition bool ≔ uProp
-definition false ≔ @prod Type Prop bool (λ x, x)
-definition true ≔ @prod Prop Prop false (λ _, false)
+definition false ≔ prod bool (λ x, x)
+definition true ≔ prod false (λ _, false)
 
-definition imp (P Q: Term uProp) ≔ @prod Prop Prop P (λ_, Q)
-definition forall {T: Term uType} (P: Term T ⇒ Term bool) ≔ @prod _ _ T P
+definition imp (P Q: Term uProp) ≔ prod P (λ_, Q)
+definition forall {T: Term uType} (P: Term T ⇒ Term bool) ≔ prod T P
 
-definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)
+definition bnot (P: Term uProp) ≔ prod P (λ _, false)
 set prefix 5 "¬" ≔ bnot
 
 definition band (P Q: Term uProp) ≔ bnot (imp P (bnot Q))