notation > "'Eq' term 90 A term 90 B"
non associative with precedence 40 for @{'myeq ? $A $B}.
-naxiom bool_ext : ∀P,Q: Prop. (P → Q) → (Q → P) → P = Q.
+naxiom bool_ext : ∀P,Q: o. (P → Q) → (Q → P) → P = Q.
naxiom f_ext_1 : ∀a,b:Type[0].∀f,g: a → b. (∀x.f x = g x) → f = g.