Opening encoding in resulting file

proofs/pipeline/examples/ex/ex.expected

+require open qfo.encoding.lhol qfo.encoding.propositional_connectives;
 symbol exi!1 : @Prf (@imp (imp qfo.spec.main.P qfo.spec.main.P) (@imp (disj (not qfo.spec.main.P) qfo.spec.main.P) (@imp (imp qfo.spec.main.P qfo.spec.main.P) (ex prop (λ (_ : El prop), imp qfo.spec.main.P qfo.spec.main.P))))) ≔
 begin
   why3;

proofs/pipeline/examples/hello/hello.expected

+require open qfo.encoding.lhol qfo.encoding.propositional_connectives;
 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;

proofs/pipeline/pipe.ml

@@ -38,6 +38,8 @@ let process proveit src qfo_conf =
     collect stdout
       (echo json |. mkprops |. foise |. chainprops depfile |. appaxiom |. solve)
   in
+  Format.printf
+    "require open qfo.encoding.lhol qfo.encoding.propositional_connectives;@\n";
   Format.printf "%s" sttprops
 
 open Cmdliner