diff --git a/proofs/chainprops/chainprops.ml b/proofs/chainprops/chainprops.ml
index 1405ebe5110e49dc55d2a1982b2fd9d6cf3fe8df..94ebc344ff77865fdc3a4a63a25bf06ec1f21ce7 100644
--- a/proofs/chainprops/chainprops.ml
+++ b/proofs/chainprops/chainprops.ml
@@ -70,7 +70,7 @@ let propositions (ast : S.ast) : decl list =
           "Invalid Dedukti source file: only symbol declarations are supported"
   in
   Stream.iter (fun c -> props := match_decl c.Pos.elt :: !props) ast;
-  !props
+  List.rev !props
 
 (** [merge imp deps props] transform each proposition of [props] into
     implications (the implication is defined by [imp]) from its
@@ -142,7 +142,7 @@ let cmd =
       `Pre "symbol tgt: P;\nsymbol hyp0: H0;\nsymbol hyp1: H1;";
       `P "$(b,psnj-chainprops foo.dep) outputs";
       `Pre
-        "symbol hyp1: H1;\nsymbol hyp0: H0;\nsymbol tgt: @imp H0 (@imp H1 P);";
+        "symbol hyp0: H0;\nsymbol hyp1: H1;\nsymbol tgt: @imp H0 (@imp H1 P);";
     ]
   in
   ( Term.(const chainprops $ deps $ imply $ pp_deps),
diff --git a/proofs/chainprops/chainprops.opam b/proofs/chainprops/chainprops.opam
index 79bc42c721470c50b69bc6a29e28d04a116572c5..d3041df5a01cf186aef8a6e2628e5b987f63762d 100644
--- a/proofs/chainprops/chainprops.opam
+++ b/proofs/chainprops/chainprops.opam
@@ -6,6 +6,7 @@ depends: [
   "dune" {>= "2.9"}
   "cmdliner"
   "angstrom"
+  "lambdapi"
   "odoc" {with-doc}
 ]
 build: [
diff --git a/proofs/chainprops/test/run.t b/proofs/chainprops/test/run.t
index 2968cc957bc1686561dbf923aab9775ca6cf4bae..c253b0459675dd7f2a6276151735ec813947f452 100644
--- a/proofs/chainprops/test/run.t
+++ b/proofs/chainprops/test/run.t
@@ -1,12 +1,12 @@
   $ ../chainprops.exe example.dep < example.lp
-  symbol hyp1: H1;
-  symbol hyp0: H0;
   symbol tgt: @imp H0 (@imp H1 P);
+  symbol hyp0: H0;
+  symbol hyp1: H1;
 
 
   $ ../chainprops.exe foo.dep < foo.lp
-  symbol nitz: Nitz;
-  symbol frob: Frob;
-  symbol baz: Baz;
-  symbol bar: @imp Frob (@imp Nitz (@imp Baz Bar));
   symbol foo: @imp Bar (@imp Baz Foo);
+  symbol bar: @imp Frob (@imp Nitz (@imp Baz Bar));
+  symbol baz: Baz;
+  symbol frob: Frob;
+  symbol nitz: Nitz;