diff --git a/proofs/qfo/lib/transpile.ml b/proofs/qfo/lib/transpile.ml
index 932eb6a77d33ee717630abf0e3e1258659620959..37bf94c6b002b405fa2bd7356047431a650b44a8 100644
--- a/proofs/qfo/lib/transpile.ml
+++ b/proofs/qfo/lib/transpile.ml
@@ -45,13 +45,16 @@ let translate_term ~(ps : E.predicate_subtyping) ~(pvs_c : E.connectives)
         let new_sym = List.assq i binary in
         T.add_args (T.mk_Symb new_sym) [ f l; f r ]
     (* Mapping quantifiers *)
+    | Symb s, [ a; t ] when s == pvs_c.existential ->
+        T.add_args (T.mk_Symb prop_c.existential) [ f a; f t ]
+    | Symb s, [ a; t ] when s == pvs_c.universal ->
+        T.add_args (T.mk_Symb prop_c.universal) [ f a; f t ]
     | Symb s, _ when s == ps.subset ->
         Format.eprintf
           "PVS-Cert pair, fst and snd cannot be translated to propositional \
-           logic@.";
+           logic (yet)@.";
         raise (CannotTranslate t)
     | u, args ->
-        let args = List.map f args in
         let hd =
           match T.unfold u with
           | Abst (a, b) ->
@@ -67,6 +70,6 @@ let translate_term ~(ps : E.predicate_subtyping) ~(pvs_c : E.connectives)
           | Vari _ | Symb _ -> u
           | _ -> assert false
         in
-        T.add_args hd args
+        T.add_args hd (List.map f args)
   in
   f t
diff --git a/proofs/qfo/test/qfo.t b/proofs/qfo/test/qfo.t
index 1e69fd2c698f65ff7b33d08bb6be5fd9226bbd98..f437d2ebcc01575c2605a5293857d500513bdcee 100644
--- a/proofs/qfo/test/qfo.t
+++ b/proofs/qfo/test/qfo.t
@@ -1,11 +1,15 @@
   $ psnj-qfo qfo.json < false.lp
   Loaded package file from "$TESTCASE_ROOT"
-  symbol false: @∀ prop (λ p: El prop, p);
-  symbol true: @∀ prop (λ p: El prop, imp p p);
+  symbol false: all prop (λ p: El prop, p);
+  symbol true: all prop (λ p: El prop, imp p p);
 
   $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj-qfo qfo.json
   Loaded package file from "$TESTCASE_ROOT"
-  symbol tt: @∀ prop (λ p: El prop, conj p p);
+  symbol tt: all prop (λ p: El prop, conj p p);
+
+  $ echo 'symbol tt: ∃ {prop} (λ p: El prop, p);' | psnj-qfo qfo.json
+  Loaded package file from "$TESTCASE_ROOT"
+  symbol tt: ex prop (λ p: El prop, p);
 
   $ psnj-qfo -e 'require open qfo.spec.withsymb;' qfo.json < withsymb_thms.lp
   Loaded package file from "$TESTCASE_ROOT"