prenex notations (adapted to lambdapi issue)

encodings/prenex.lp

@@ -3,14 +3,16 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
 set declared "χ"
-set declared "∇"
+set declared "∀S"
+set declared "∀B"
+
 symbol Scheme: TYPE
 symbol χ: Scheme → TYPE
-symbol ∇: Set → Scheme
-rule χ (∇ $X) ↪ η $X
+symbol scheme: Set → Scheme
+rule χ (scheme $X) ↪ η $X
 
-constant symbol forallS: (Set → Scheme) → Scheme
-rule χ (forallS $p) ↪ ΠT: Set, χ ($p T)
+constant symbol ∀S: (Set → Scheme) → Scheme
+rule χ (∀S $p) ↪ ΠT: Set, χ ($p T)
 
-constant symbol forallB: (Set → Bool) → Bool
-rule ε (forallB $P) ↪ Πx: Set, ε ($P x)
+constant symbol ∀B: (Set → Bool) → Bool
+rule ε (∀B $P) ↪ Πx: Set, ε ($P x)

paper/equal.lp

 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
-require personoj.encodings.prenex as P
+require open personoj.encodings.prenex
 
-symbol eq: P.χ (P.forallS (λT: ϕ {|set|}, P.∇ (T ~> T ~> bool)))
+symbol eq: χ (∀S (λT: ϕ {|set|}, scheme (T ~> T ~> bool)))