from Framework/specs/logics/first-order/syntax/fol get Base2FOL
from Framework/specs/logics/first-order/model_theory/fol get FOLMODView
from Framework/specs/logics/first-order/proof_theory/fol get FOL2FOLPF
newcomorphism ERR =
meta LF
source FOL1
target PL1
syntax NS
models NS
proofs PS
end