ad-hoc polymorphism is prenex

encodings/ad_hoc.lp

-require open personoj.encodings.lhol
-             personoj.encodings.pvs_cert
-             personoj.encodings.subtype
-             personoj.encodings.equality
+// Prenex ad-hoc polymorphism
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+  personoj.encodings.equality
+  personoj.encodings.prenex
+  personoj.encodings.subtype
 
-symbol forall_sub: Set ⇒ (Set ⇒ Set) ⇒ Set
-rule η (forall_sub &T &C) → ∀U: Set, ε (U ⊑ &T) ⇒ η (&C U)
+symbol forallah_scheme: Set ⇒ (Set ⇒ Scheme) ⇒ Scheme
+rule χ (forallah_scheme &T &C) → ∀U: Set, ε (U ⊑ &T) ⇒ χ (&C U)
+
+symbol forallah_bool: Set ⇒ (Set ⇒ Bool) ⇒ Bool
+rule ε (forallah_bool &T &C) → ∀U: Set, ε (U ⊑ &T) ⇒ ε (&C U)

encodings/prenex.lp

-require open personoj.encodings.lhol personoj.encodings.pvs_cert
+// Prenex polymorphism
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
 
 set declared "χ"
 set declared "∇"