diff --git a/proofs/pipeline/examples/encoding/cpl.lp b/proofs/pipeline/examples/encoding/cpl.lp
index e1372dbf4edf48a29953ff651813ab57bdafd9ad..b7610a3e374be0d5dbd2e6218b3104509d14c881 100644
--- a/proofs/pipeline/examples/encoding/cpl.lp
+++ b/proofs/pipeline/examples/encoding/cpl.lp
@@ -1,6 +1,6 @@
 // Constructive propositional calculus
 // TODO: define the connectives
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;
diff --git a/proofs/pipeline/examples/encoding/propositional_connectives.lp b/proofs/pipeline/examples/encoding/propositional_connectives.lp
index cc05c0c6400bb223c7a02b9a42a3fec19a4c10be..cff262279cf673d2c3951eb08e1d523a26f7de61 100644
--- a/proofs/pipeline/examples/encoding/propositional_connectives.lp
+++ b/proofs/pipeline/examples/encoding/propositional_connectives.lp
@@ -1,7 +1,7 @@
 // Klassische propositional logic
 // TODO: define connectives using constructive ones
-require open qfo.lhol;
-require qfo.cpl as C;
+require open qfo.encoding.lhol;
+require qfo.encoding.cpl as C;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;
@@ -12,9 +12,13 @@ constant symbol not: Prop → Prop;
 constant symbol ex: Set → (Set → Prop) → Prop;
 constant symbol all: Set → (Set → Prop) → Prop;
 
+//builtin "T" ≔ El;
+//builtin "P" ≔ Prf;
 builtin "imp" ≔ imp;
 builtin "bot" ≔ bot;
 builtin "top" ≔ top;
 builtin "and" ≔ conj;
 builtin "or" ≔ disj;
 builtin "not" ≔ not;
+
+opaque symbol ok : Prf (∀ {prop} (λ (x: El prop), imp x x)) ≔ begin assume x; why3; end;
diff --git a/proofs/pipeline/examples/encoding/pvs_cert.lp b/proofs/pipeline/examples/encoding/pvs_cert.lp
index d8b4df5f21d3b1e51a985b4b14e34ec90c91ab3a..ce06190848c1318b340fc08e83caa996039527cb 100644
--- a/proofs/pipeline/examples/encoding/pvs_cert.lp
+++ b/proofs/pipeline/examples/encoding/pvs_cert.lp
@@ -1,5 +1,5 @@
 // PVS-Cert
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol psub {x: Set}: (El x → Prop) → Set;
 protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);
diff --git a/proofs/pipeline/examples/encoding/pvs_connectives.lp b/proofs/pipeline/examples/encoding/pvs_connectives.lp
index 6f95f3f730a274f42072ed36eb7fabca313fffbb..a6351c2d370c6e5a3561b34fedee9e5f321f3acd 100644
--- a/proofs/pipeline/examples/encoding/pvs_connectives.lp
+++ b/proofs/pipeline/examples/encoding/pvs_connectives.lp
@@ -1,5 +1,5 @@
 // Definition based on implication
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 symbol false ≔ ∀ {prop} (λ x: El prop, x);
 symbol true ≔ false ⇒ (λ _: Prf false, false);
diff --git a/proofs/pipeline/examples/lambdapi.pkg b/proofs/pipeline/examples/lambdapi.pkg
new file mode 100644
index 0000000000000000000000000000000000000000..a5da49bb7e2ce5ba8839767c345f5827ae05e243
--- /dev/null
+++ b/proofs/pipeline/examples/lambdapi.pkg
@@ -0,0 +1,2 @@
+root_path = qfo
+package_name = qfo
diff --git a/proofs/pipeline/examples/run.expected b/proofs/pipeline/examples/run.expected
index e3eae81838984cd5d539a2252502ee623e3e612c..e3dd0e12f1abf66e8eaff8fb9f461344b9524eb9 100644
--- a/proofs/pipeline/examples/run.expected
+++ b/proofs/pipeline/examples/run.expected
@@ -1,24 +1,24 @@
-symbol hello!1 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!1 : @Prf (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (imp qfo.spec.main.P (imp qfo.spec.main.Q (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!2 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!2 : @Prf (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (imp qfo.spec.main.P (imp qfo.spec.main.Q (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!3 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!3 : @Prf (@imp (disj qfo.spec.main.P (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (@imp (disj qfo.spec.main.Q (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!4 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!4 : @Prf (@imp (disj qfo.spec.main.P (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (@imp (disj qfo.spec.main.Q (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!5 : @Prf (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) ≔
+symbol hello!5 : @Prf (disj qfo.spec.main.P (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) ≔
 begin
   why3;
 end;
-symbol hello!6 : @Prf (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) ≔
+symbol hello!6 : @Prf (disj qfo.spec.main.Q (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) ≔
 begin
   why3;
 end;
\ No newline at end of file
diff --git a/proofs/pipeline/examples/run.sh b/proofs/pipeline/examples/run.sh
index 4ca8b020e1df6e7899f70e8368752fe507ec148c..7f052f849945a6a3679945edaa53cf055374a41d 100644
--- a/proofs/pipeline/examples/run.sh
+++ b/proofs/pipeline/examples/run.sh
@@ -1,3 +1,3 @@
 #!/bin/sh
 set -euf
-opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log encoding/ spec/
+opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log
diff --git a/proofs/pipeline/examples/spec/main.lp b/proofs/pipeline/examples/spec/main.lp
index 98a4f22ac7f23c7c6ec3353a15c0eb344773b2db..c4cfc952b8f6bbcc30502121a2f1825d9c7c4b18 100644
--- a/proofs/pipeline/examples/spec/main.lp
+++ b/proofs/pipeline/examples/spec/main.lp
@@ -1,3 +1,3 @@
-require open qfo.lhol qfo.pvs_cert;
+require open qfo.encoding.lhol qfo.encoding.pvs_cert;
 symbol P: Prop;
 symbol Q: Prop;
diff --git a/proofs/pipeline/pipe.ml b/proofs/pipeline/pipe.ml
index 6aa85f134fe9a115134bf6dbb517743478485b68..8ac1ce5fbd3627863a17013ae62c02d0b2393065 100644
--- a/proofs/pipeline/pipe.ml
+++ b/proofs/pipeline/pipe.ml
@@ -1,7 +1,7 @@
 open Feather
 open Feather.Infix
 
-let process proveit src qfo_conf encoding specification =
+let process proveit src qfo_conf =
   (* Define commands *)
   let proveit =
     Option.map (fun p -> process p [ "--traces"; "-l"; src ]) proveit
@@ -19,12 +19,8 @@ let process proveit src qfo_conf encoding specification =
     process "psnj-qfo"
       [
         qfo_conf;
-        "--map-dir";
-        "qfo:" ^ encoding;
-        "--map-dir";
-        "spec:" ^ specification;
         "-e";
-        "require open spec.main;";
+        "require open qfo.spec.main;";
       ]
   and chainprops depfile = process "psnj-chainprops" [ depfile ]
   and appaxiom = process "psnj-appaxiom" [ "-a"; "Prf" ] 
@@ -59,16 +55,6 @@ let qfo_conf =
   let doc = "Configuration for QFO" in
   Arg.(value & opt string "qfo.json" & info [ "qfo" ] ~doc)
 
-let encoding =
-  let doc =
-    "Use encoding $(docv) to translate files from full blown PVS-Cert to STT."
-  in
-  Arg.(required & pos 1 (some dir) None & info [] ~doc ~docv:"ENC")
-
-let specification =
-  let doc = "Open module $(docv).main to translate propositions" in
-  Arg.(required & pos 2 (some dir) None & info [] ~doc ~docv:"MOD")
-
 let proveit =
   let doc = "Execute $(docv) to obtain a log file with proof information" in
   Arg.(value & opt (some string) None & info [ "proveit" ] ~doc ~docv:"FILE")
@@ -77,7 +63,7 @@ let cmd =
   let exits = Term.default_exits in
   let doc = "Pipeline for personoj" in
   let man = [] in
-  ( Term.(const process $ proveit $ src $ qfo_conf $ encoding $ specification),
+  ( Term.(const process $ proveit $ src $ qfo_conf),
     Term.(info "psnj-pipe" ~exits ~doc ~man) )
 
 let () = Term.(exit @@ eval cmd)
diff --git a/proofs/qfo/bin/main.ml b/proofs/qfo/bin/main.ml
index 95b6e7962cfa7c4b283c18db38d53ab0ffaa05e3..ae61cdc50fa70fe48ce17bcc99b7a80d188c00e8 100644
--- a/proofs/qfo/bin/main.ml
+++ b/proofs/qfo/bin/main.ml
@@ -86,7 +86,8 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
       let ss = new_sig_state mp in
       let ast =
         Parser.parse_string "<qfo>"
-          "require open qfo.lhol qfo.pvs_cert qfo.pvs_connectives;"
+          "require open qfo.encoding.lhol qfo.encoding.pvs_cert \
+           qfo.encoding.pvs_connectives;"
       in
       compile_ast ss ast
     with Error.Fatal (pos, msg) ->
@@ -102,7 +103,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
            let ss = new_sig_state mp in
            let ast =
              Parser.parse_string "<qfo>"
-               "require open qfo.lhol qfo.pvs_connectives;"
+               "require open qfo.encoding.lhol qfo.encoding.pvs_connectives;"
            in
            compile_ast ss ast
          with Error.Fatal (p, m) ->
@@ -116,7 +117,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
     let ss = new_sig_state mp in
     let ast =
       Parser.parse_string "<qfo>"
-        "require open qfo.lhol qfo.propositional_connectives;"
+        "require open qfo.encoding.lhol qfo.encoding.propositional_connectives;"
     in
     compile_ast ss ast
   in
@@ -131,7 +132,8 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
       let ss = new_sig_state [ "<qfo>" ] in
       let ast =
         Parser.parse_string "<qfo>"
-          "require open qfo.lhol qfo.pvs_cert qfo.pvs_connectives;"
+          "require open qfo.encoding.lhol qfo.encoding.pvs_cert \
+           qfo.encoding.pvs_connectives;"
       in
       compile_ast ss ast
     with Error.Fatal (p, m) ->
@@ -160,7 +162,8 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
     try
       let ss = new_sig_state [ "<qfo.print>" ] in
       let open_cmd =
-        "require open qfo.lhol qfo.pvs_cert qfo.propositional_connectives;"
+        "require open qfo.encoding.lhol qfo.encoding.pvs_cert \
+         qfo.encoding.propositional_connectives;"
       in
       compile_ast ss (Parser.parse_string "<qfo.print>" open_cmd)
     with Error.Fatal (p, msg) ->
@@ -206,6 +209,11 @@ let cmd =
          in PVS-Cert with dependent logical connectives into a list of axioms \
          expressed in something close to simple type theory with non dependent \
          logical connectives."
+    ; `P
+        "The program requires all its source files to be in the package \
+         $(b,qfo). The easiest way to do that is to place the source files in \
+         a directory where there is a $(b,lambdapi.pkg) file with the line \
+         $(b,root_path=qfo)."
     ; `P
         "To convert files, the program needs identify the symbols of the \
          encoding. The mapping allows to indicate the name of such symbols. \
@@ -238,9 +246,16 @@ let cmd =
          \"pvs_connectives\" and \"propositional_connectives\" define logical \
          connectors: connectors from \"pvs_connectives\" are replaced by \
          connectors from \"propositional_connectives\"."
+    ; `P
+        "Symbols mentioned in $(b,\"pvs_cert\") are expected to be found in \
+         modules $(b,qfo.encoding.pvs_cert) and $(b,qfo.encoding.lhol), \
+         symbols mentioned in $(b,\"pvs_connectives\") are expected to be \
+         found in module $(b,qfo.encoding.pvs_connectives) and symbols \
+         mentioned in $(b,\"propositional_connectives\") are expected to be \
+         found in module $(b,qfo.encoding.proposisitional_connectives)."
     ; `P
         "Furthermore, if the standard input uses symbols from some other \
-         module \"mod\", it can be opened using $(b,-e mod)."
+         module \"mod\", it can be opened using $(b,-e 'require open mod;')."
     ; `S Manpage.s_examples
     ; `P "Let qfo.json be the following json file"
     ; `Pre
@@ -285,9 +300,6 @@ let cmd =
     ; `P "The program outputs"
     ; `Pre "symbol true: @∀ prop (λ p: El prop, imp p p);"
     ; `S Manpage.s_bugs
-    ; `P
-        "Unlike in lambdapi, because standard input is parsed, the option \
-         $(b,--map-dir) should in general be used."
     ; `P
         "If the input opens some module (using \"open mod\"), then symbols \
          from this module will appear fully qualified."
diff --git a/proofs/qfo/test/encoding/cpl.lp b/proofs/qfo/test/encoding/cpl.lp
index e1372dbf4edf48a29953ff651813ab57bdafd9ad..b7610a3e374be0d5dbd2e6218b3104509d14c881 100644
--- a/proofs/qfo/test/encoding/cpl.lp
+++ b/proofs/qfo/test/encoding/cpl.lp
@@ -1,6 +1,6 @@
 // Constructive propositional calculus
 // TODO: define the connectives
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;
diff --git a/proofs/qfo/test/encoding/propositional_connectives.lp b/proofs/qfo/test/encoding/propositional_connectives.lp
index cc05c0c6400bb223c7a02b9a42a3fec19a4c10be..47ad7e38b11f7c126463f4650c9630422a1c4ccc 100644
--- a/proofs/qfo/test/encoding/propositional_connectives.lp
+++ b/proofs/qfo/test/encoding/propositional_connectives.lp
@@ -1,7 +1,7 @@
 // Klassische propositional logic
 // TODO: define connectives using constructive ones
-require open qfo.lhol;
-require qfo.cpl as C;
+require open qfo.encoding.lhol;
+require qfo.encoding.cpl as C;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;
diff --git a/proofs/qfo/test/encoding/pvs_cert.lp b/proofs/qfo/test/encoding/pvs_cert.lp
index 2e9091f51c527252d0a6bc075b86568a1090a053..fde15e9e04d45cd9025e40be9b7358e45b466014 100644
--- a/proofs/qfo/test/encoding/pvs_cert.lp
+++ b/proofs/qfo/test/encoding/pvs_cert.lp
@@ -1,5 +1,5 @@
 // PVS-Cert
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol psub {x: Set}: (El x → Prop) → Set;
 protected constant symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);
diff --git a/proofs/qfo/test/encoding/pvs_connectives.lp b/proofs/qfo/test/encoding/pvs_connectives.lp
index 6f95f3f730a274f42072ed36eb7fabca313fffbb..a6351c2d370c6e5a3561b34fedee9e5f321f3acd 100644
--- a/proofs/qfo/test/encoding/pvs_connectives.lp
+++ b/proofs/qfo/test/encoding/pvs_connectives.lp
@@ -1,5 +1,5 @@
 // Definition based on implication
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 symbol false ≔ ∀ {prop} (λ x: El prop, x);
 symbol true ≔ false ⇒ (λ _: Prf false, false);
diff --git a/proofs/qfo/test/qfo.t b/proofs/qfo/test/qfo.t
index 2ae8895af0b8f7923fefb8d7b21256eeac6c2fc4..3c5d63c21a3048f9a0f602a3dcb59da786ee266e 100644
--- a/proofs/qfo/test/qfo.t
+++ b/proofs/qfo/test/qfo.t
@@ -1,9 +1,9 @@
-  $ psnj-qfo --map-dir=qfo:encoding qfo.json < false.lp
+  $ psnj-qfo qfo.json < false.lp 2>'/dev/null'
   symbol false: @∀ prop (λ p: El prop, p);
   symbol true: @∀ prop (λ p: El prop, imp p p);
 
-  $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj-qfo --map-dir=qfo:encoding qfo.json
+  $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj-qfo qfo.json 2>'/dev/null'
   symbol tt: @∀ prop (λ p: El prop, conj p p);
 
-  $ psnj-qfo --map-dir=qfo:encoding --map-dir=spec:spec -e 'require open spec.withsymb;' qfo.json < withsymb_thms.lp
-  symbol trivial: imp spec.withsymb.P spec.withsymb.P;
+  $ psnj-qfo -e 'require open qfo.spec.withsymb;' qfo.json < withsymb_thms.lp 2>'/dev/null'
+  symbol trivial: imp qfo.spec.withsymb.P qfo.spec.withsymb.P;
diff --git a/proofs/qfo/test/spec/withsymb.lp b/proofs/qfo/test/spec/withsymb.lp
index bacd6abcbecfb3322cb071f4c95fc5b4474c6b64..856740a7907ca52ee10be58267f71c1e46c60c3a 100644
--- a/proofs/qfo/test/spec/withsymb.lp
+++ b/proofs/qfo/test/spec/withsymb.lp
@@ -1,3 +1,3 @@
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 symbol P: Prop;
 symbol trivial: Prf (P ⇒ (λ _: Prf P, P));