prefixing import to launch lp from git root

prelude/boolean_props.lp

-require open pvs_core booleans equalities if_def
+require open pvs_core prelude.booleans prelude.equalities prelude.if_def
 
 // true /= false
 symbol bool_inclusive : eps (bnot (eq bool false true))

prelude/equalities.lp

-require open pvs_core booleans
+require open pvs_core prelude.booleans
 
 symbol eq : ∀ T : Type, eta T ⇒ eta T ⇒ eta bool

prelude/if_def.lp

-require open pvs_core booleans equalities notequal
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
 
 symbol if (T:Type): eta bool ⇒ eta T ⇒ eta T ⇒ eta T

prelude/notequal.lp

-require open pvs_core booleans equalities
+require open pvs_core prelude.booleans prelude.equalities
 
 definition neq (T: Type) (x: eta T) (y: eta T) ≔ bnot (eq T x y)

prelude/prelude.lp

-require open pvs_core booleans equalities notequal if_def
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
+require open prelude.if_def

prelude/rat.lp

-require open pvs_core booleans equalities notequal
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
 
 constant symbol rat : Type
 constant symbol zero : eta rat