fixed equality

87598969 · gabrielhdt · c89e0b0f · 87598969
Commit 87598969 authored 4 years ago by gabrielhdt
--- a/paper/equal.lp
+++ b/paper/equal.lp
-require open
-personoj.encodings.lhol
-personoj.encodings.pvs_cert
-personoj.paper.prenex
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require personoj.encodings.prenex as P

-symbol eq: χ (forall_pt (λT: ϕ ctype, ∇ (T ~> T ~> cbool)))
+symbol eq: P.χ (P.forallS (λT: ϕ {|set|}, P.∇ (T ~> T ~> bool)))