diff --git a/src/common/debug.ml b/src/common/debug.ml
index a6f18e329..849414b52 100644
--- a/src/common/debug.ml
+++ b/src/common/debug.ml
@@ -26,7 +26,7 @@ module D = struct
     | Some x -> out ppf "Some(%a)" elt x
 
   let pair : 'a pp -> 'b pp -> ('a * 'b) pp = fun elt1 elt2 ppf (x1,x2) ->
-    out ppf "%a,%a" elt1 x1 elt2 x2
+    out ppf "(%a,%a)" elt1 x1 elt2 x2
 
   let list : 'a pp -> 'a list pp = fun elt ppf l ->
     match l with
diff --git a/src/handle/fol.ml b/src/handle/fol.ml
index 78e54c0ef..31776f9ee 100644
--- a/src/handle/fol.ml
+++ b/src/handle/fol.ml
@@ -1,15 +1,18 @@
 (** Configuration for tactics based on first-order logic. *)
 
-open Common
+open Common open Error
 open Core open Term
 
 (** Builtin configuration for propositional logic. *)
 type config =
-  { symb_P   : sym (** Encoding of propositions. *)
+  { symb_Prop: sym (** Type of propositions. *)
+  ; symb_P   : sym (** Encoding of propositions. *)
+  ; symb_Set : sym (** Type of sets. *)
   ; symb_T   : sym (** Encoding of types. *)
   ; symb_or  : sym (** Disjunction(∨) symbol. *)
   ; symb_and : sym (** Conjunction(∧) symbol. *)
   ; symb_imp : sym (** Implication(⇒) symbol. *)
+  ; symb_eqv : sym (** Equivalence(⇔) symbol. *)
   ; symb_bot : sym (** Bot(⊥) symbol. *)
   ; symb_top : sym (** Top(⊤) symbol. *)
   ; symb_not : sym (** Not(¬) symbol. *)
@@ -19,11 +22,38 @@ type config =
 (** [get_config ss pos] build the configuration using [ss]. *)
 let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos ->
   let builtin = Builtin.get ss pos in
-  { symb_P   = builtin "P"
-  ; symb_T   = builtin "T"
+  let symb_P = builtin "P" and symb_T = builtin "T" in
+  let symb_Prop =
+    match unfold Timed.(!(symb_P.sym_type)) with
+    | Prod(a,_) ->
+        begin
+          match unfold a with
+          | Symb s -> s
+          | _ ->
+              fatal pos "The type of %a is not of the form Prop → _ \
+                         with Prop a symbol." Print.sym symb_P
+        end
+    | _ -> fatal pos "The type of %a is not a product" Print.sym symb_P
+  and symb_Set =
+    match unfold Timed.(!(symb_T.sym_type)) with
+    | Prod(a,_) ->
+        begin
+          match unfold a with
+          | Symb s -> s
+          | _ ->
+              fatal pos "The type of %a is not of the form Prop → _ \
+                         with Prop a symbol." Print.sym symb_T
+        end
+    | _ -> fatal pos "The type of %a is not a product" Print.sym symb_T
+  in
+  { symb_Prop
+  ; symb_P
+  ; symb_Set
+  ; symb_T
   ; symb_or  = builtin "or"
   ; symb_and = builtin "and"
   ; symb_imp = builtin "imp"
+  ; symb_eqv = builtin "eqv"
   ; symb_bot = builtin "bot"
   ; symb_top = builtin "top"
   ; symb_not = builtin "not"
diff --git a/src/handle/rewrite.ml b/src/handle/rewrite.ml
index 11acc0971..812c2038b 100644
--- a/src/handle/rewrite.ml
+++ b/src/handle/rewrite.ml
@@ -30,7 +30,7 @@ let get_eq_config : Sig_state.t -> popt -> eq_config = fun ss pos ->
 
 (* Register checks for the builtin symbols related to rewriting. *)
 let _ =
-  let check_t_or_p _ss pos sym =
+  let check_codomain_is_Type _ss pos sym =
     let valid =
       match Eval.whnf [] !(sym.sym_type) with
       | Prod(_, b) -> Eval.eq_modulo [] (snd (Bindlib.unbind b)) mk_Type
@@ -40,9 +40,9 @@ let _ =
       fatal pos "The type of [%s] is not of the form [_ → TYPE]." sym.sym_name
   in
   (* The type of the builtin ["T"] should be [U → TYPE]. *)
-  Builtin.register "T" check_t_or_p;
+  Builtin.register "T" check_codomain_is_Type;
   (* The type of the builtin ["P"] should be [Prop → TYPE]. *)
-  Builtin.register "P" check_t_or_p;
+  Builtin.register "P" check_codomain_is_Type;
   let get_domain_of_type s =
     match Eval.whnf [] !(s.sym_type) with
     | Prod(a,_) -> a
diff --git a/src/handle/why3_tactic.ml b/src/handle/why3_tactic.ml
index 2e2068893..598af4431 100644
--- a/src/handle/why3_tactic.ml
+++ b/src/handle/why3_tactic.ml
@@ -1,14 +1,15 @@
 (** Implementation of the why3 tactic. *)
 
-open Lplib open Extra
+open Lplib
 open Timed
 open Common open Error
 open Core open Term open Print
 open Fol
+open Proof
 
 (** Logging function for external prover calling with Why3. *)
-let log_why3 = Logger.make 'y' "why3" "why3 provers"
-let log_why3 = log_why3.pp
+let log = Logger.make 'y' "why3" "why3 provers"
+let log = log.pp
 
 (** [default_prover] contains the name of the current prover. Note that it can
     be changed by using the "set prover <string>" command. *)
@@ -36,166 +37,352 @@ let why3_main : Why3.Whyconf.main = Why3.Whyconf.get_main why3_config
 let why3_env : Why3.Env.env =
   Why3.Env.create_env (Why3.Whyconf.loadpath why3_main)
 
-(** A map from lambdapi terms to Why3 constants. *)
-type cnst_table = (term * Why3.Term.lsymbol) list
-
-(** Table of declared types, these types may be variables or constants. *)
-module TyTable : sig
-  type t
-
-  val empty : t
-
-  val ty_of_term : t -> term -> t * Why3.Ty.ty
-  (** [ty_of_term tbl te] fetches the type associated to term [te] in
-      table [tbl] if it exists, or it creates such a type and return
-      the created type and the new table. *)
-
-  (** {b FIXME} the translation of types {!ty_of_term} is correct on
-      non empty types only. *)
-
-  val fold_left :
-    do_var:('a -> term -> Why3.Ty.tvsymbol -> 'a) ->
-    do_sym:('a -> term -> Why3.Ty.tysymbol -> 'a) -> 'a -> t -> 'a
-  (** [fold_left ~do_var ~do_sym init tbl] folds over the table [tbl]
-      with initial value [init] using [do_var] to operate on type
-      variables and [do_sym] to operate on type symbols. *)
-end = struct
-  (* The module is created to hide the type [sym_or_var] *)
-  type sym_or_var = TySym of Why3.Ty.tysymbol | TyVar of Why3.Ty.tvsymbol
-
-  type t = (term * sym_or_var) list
-
-  let empty = []
-
-  let ty_of_term tbl te =
-    match List.assoc_eq (Eval.eq_modulo []) te tbl with
-    | TySym s -> (tbl, Why3.Ty.ty_app s [])
-    | TyVar v -> (tbl, Why3.Ty.ty_var v)
-    | exception Not_found -> (
-        (* FIXME generate a new goal to ensure that types translated as
-           fresh constants are inhabited. *)
-        match get_args te with
-        | Symb s, [] ->
-          let id = Why3.Ident.id_fresh s.sym_name in
-          let sym = Why3.(Ty.create_tysymbol id [] Ty.NoDef) in
-          ((te,TySym sym)::tbl, Why3.Ty.ty_app sym [])
-        | Vari x, [] ->
-          let sym = Why3.Ty.tv_of_string (Bindlib.name_of x) in
-          ((te,TyVar sym)::tbl, Why3.Ty.ty_var sym)
-        | _ ->
-          let id = Why3.Ident.id_fresh "ty" in
-          let sym = Why3.(Ty.create_tysymbol id [] Ty.NoDef) in
-          ((te,TySym sym)::tbl, Why3.Ty.ty_app sym []))
-
-  let fold_left ~do_var ~do_sym acc tbl =
-    let f acc (t,s_or_v) =
-      match s_or_v with
-      | TySym s -> do_sym acc t s
-      | TyVar v -> do_var acc t v
-    in
-    List.fold_left f acc tbl
-end
-
-(** [translate_term cfg tbl t] translates the given lambdapi term [t] into the
-    correspondig Why3 term, using the configuration [cfg] and constants in the
-    association list [tbl]. *)
-let translate_term : config -> cnst_table -> TyTable.t -> term ->
-                       (cnst_table * TyTable.t * Why3.Term.term) option =
-  fun cfg tbl ty_tbl t ->
-  let rec translate_prop tbl ty_tbl t =
-    match get_args t with
-    | Symb(s), [t1; t2] when s == cfg.symb_and ->
-        let (tbl, ty_tbl, t1) = translate_prop tbl ty_tbl t1 in
-        let (tbl, ty_tbl, t2) = translate_prop tbl ty_tbl t2 in
-        (tbl, ty_tbl, Why3.Term.t_and t1 t2)
-    | Symb(s), [t1; t2] when s == cfg.symb_or  ->
-        let (tbl, ty_tbl, t1) = translate_prop tbl ty_tbl t1 in
-        let (tbl, ty_tbl, t2) = translate_prop tbl ty_tbl t2 in
-        (tbl, ty_tbl, Why3.Term.t_or t1 t2)
-    | Symb(s), [t1; t2] when s == cfg.symb_imp ->
-        let (tbl, ty_tbl, t1) = translate_prop tbl ty_tbl t1 in
-        let (tbl, ty_tbl, t2) = translate_prop tbl ty_tbl t2 in
-        (tbl, ty_tbl, Why3.Term.t_implies t1 t2)
-    | Symb(s), [t] when s == cfg.symb_not ->
-        let (tbl, ty_tbl, t) = translate_prop tbl ty_tbl t in
-        (tbl, ty_tbl, Why3.Term.t_not t)
-    | Symb(s), [] when s == cfg.symb_bot ->
-        (tbl, ty_tbl, Why3.Term.t_false)
-    | Symb(s), [] when s == cfg.symb_top ->
-        (tbl, ty_tbl, Why3.Term.t_true)
-    | Symb(s), [a;Abst(_,t)] when s == cfg.symb_ex || s == cfg.symb_all ->
-        let (ty_tbl, ty) = TyTable.ty_of_term ty_tbl a in
-        let x, t = Bindlib.unbind t in
-        let (tbl, ty_tbl ,t) = translate_prop tbl ty_tbl t in
-        let tquant =
-          let id = Why3.Ident.id_fresh (Bindlib.name_of x) in
-          let vid = Why3.(Term.create_vsymbol id) ty in
-          let close =
-            if s == cfg.symb_ex then Why3.Term.t_exists_close
-            else Why3.Term.t_forall_close
-           (* Other cases excluded by pattern matching *)
-          in
-          close [vid] [] t
-        in
-        (tbl, ty_tbl, tquant)
+(** Data type used to record how Lambdapi symbols, variables and terms are
+    mapped to Why3 symbols or variables. *)
+type l2y =
+  { s2ts : (sym * Why3.Ty.tysymbol) list
+  (* Mapping of type symbols. *)
+  ; t2ts : (term * Why3.Ty.tysymbol) list
+  (* Mapping of non-Why3 subtypes. *)
+  ; v2tv : (tvar * Why3.Ty.tvsymbol) list
+  (* Mapping of type variables. *)
+  ; s2ls : (sym * (Why3.Term.lsymbol * bool)) list
+  (* Mapping of function symbols. [true] is for predicates. *)
+  ; v2ls : (tvar * (Why3.Term.lsymbol * bool)) list
+  (* Mapping of environment variables. [true] is for predicates. *)
+  ; t2ls : (term * Why3.Term.lsymbol) list
+  (* Mapping of non-Why3 subterms. *)
+  ; v2vs : (tvar * Why3.Term.vsymbol) list
+  (* Mapping of object variables. *)
+  }
+
+let empty_l2y =
+  {s2ts=[]; v2tv=[]; t2ts=[]; s2ls=[]; v2ls=[]; v2vs=[]; t2ls=[]}
+
+let l2y ppf m =
+  let open Debug.D in
+  Base.out ppf
+    "{s2ts=%a; v2tv=%a; t2ts=%a; s2ls=%a; v2ls=%a; v2vs=%a; t2ls=%a}"
+    (list (pair sym Why3.Pretty.print_ts)) m.s2ts
+    (list (pair var Why3.Pretty.print_tv)) m.v2tv
+    (list (pair term Why3.Pretty.print_ts)) m.t2ts
+    (list (pair sym (pair Why3.Pretty.print_ls bool))) m.s2ls
+    (list (pair var (pair Why3.Pretty.print_ls bool))) m.v2ls
+    (list (pair var Why3.Pretty.print_vs)) m.v2vs
+    (list (pair term Why3.Pretty.print_ls)) m.t2ls
+
+(** Translation functions below raise Exit if a term cannot be
+    translated. They return an update l2y map as well because mappings are
+    done while translating terms. *)
+
+(** [translate_set m t] tries to translate a Lambdapi term [t:Set] to a Why3
+    type. *)
+let rec translate_set m t =
+  if Logger.log_enabled() then log "translate_set %a [%a]" l2y m term t;
+  match get_args t with
+  | Symb s, ts ->
+      let m, ts = translate_sets m ts in
+      let m, s =
+        match List.assoc_opt s m.s2ts with
+        | Some s' -> m, s'
+        | None ->
+            let id = Why3.Ident.id_fresh s.sym_name in
+            let s' = Why3.Ty.create_tysymbol id [] Why3.Ty.NoDef in
+            if Logger.log_enabled() then
+              log "add tysymbol %a" Why3.Pretty.print_ts s';
+            {m with s2ts=(s,s')::m.s2ts}, s'
+      in
+      m, Why3.Ty.ty_app s ts
+  | Vari x, [] ->
+      begin
+        match List.assoc_eq_opt Bindlib.eq_vars x m.v2tv with
+        | Some tv -> m, Why3.Ty.ty_var tv
+        | None -> raise Exit
+      end
+  | _ -> raise Exit
+      (*try m, Why3.Ty.ty_app (List.assoc_eq (Eval.eq_modulo []) t m.t2ts) []
+      with Not_found ->
+        let id = Why3.Ident.id_fresh "T" in
+        let s = Why3.Ty.create_tysymbol id [] Why3.Ty.NoDef in
+        {m with t2ts = (t,s)::m.t2ts}, Why3.Ty.ty_app s []*)
+
+and translate_sets m ts =
+  List.fold_right
+    (fun t (m,ts) -> let m,t = translate_set m t in m, t::ts)
+    ts (m,[])
+
+(** [translate_type m t] tries to translate a Lambdapi term [t:TYPE] of the
+    form [P _] to a Why3 type. *)
+let translate_type cfg m t =
+  if Logger.log_enabled() then log "translate_type %a [%a]" l2y m term t;
+  match get_args t with
+  | Symb s, [t] when s == cfg.symb_T -> translate_set m t
+  | _ -> raise Exit
+
+(*let translate_types cfg m ts =
+  List.fold_right
+    (fun t (m,ts) -> let m,t = translate_type cfg m t in m, t::ts)
+    ts (m,[])*)
+
+(** [translate_pred_type cfg m t] tries to translate a Lambdapi term [t] of
+    the form [T a1 → .. → T an → Prop] to a Why3 type. *)
+let translate_pred_type cfg =
+  let rec aux acc m t =
+    if Logger.log_enabled() then
+      log "translate_pred_type %a [%a]" l2y m term t;
+    match unfold t with
+    | Symb s -> if s == cfg.symb_Prop then m, List.rev acc else raise Exit
+    | Prod(a,b) ->
+        let m,a = translate_type cfg m a in
+        let _,b = Bindlib.unbind b in
+        aux (a::acc) m b
+    | _ -> raise Exit
+  in aux []
+
+(** [translate_fun_type cfg m t] tries to translate a Lambdapi term [t] of the
+    form [T a1 → .. → T an → T a] to a Why3 type. *)
+let translate_fun_type cfg =
+  let rec aux acc m t =
+    if Logger.log_enabled() then
+      log "translate_fun_type %a [%a]" l2y m term t;
+    match unfold t with
+    | Prod(a,b) ->
+        let m,a = translate_type cfg m a in
+        let _,b = Bindlib.unbind b in
+        aux (a::acc) m b
     | _ ->
-        (* If the term [p] is mapped in [tbl] then use it. *)
-        try
-          let sym = List.assoc_eq (Eval.eq_modulo []) t tbl in
-          (tbl, ty_tbl, Why3.Term.ps_app sym [])
-        with Not_found ->
-          (* Otherwise generate a new constant in why3. *)
-          let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "P") [] in
-          ((t, sym)::tbl, ty_tbl, Why3.Term.ps_app sym [])
+        let m,a = translate_type cfg m t in
+        m, List.rev acc, a
+  in aux []
+
+(** [translate_term cfg m t] tries to translate a Lambdapi term [t:T _] to a
+    Why3 term. *)
+let rec translate_term cfg m t =
+  if Logger.log_enabled() then log "translate_term %a [%a]" l2y m term t;
+  match get_args t with
+  | Symb s, ts ->
+      begin
+        match List.assoc_eq_opt (==) s m.s2ls with
+        | Some(_, true) -> assert false
+        | Some(s, false) ->
+            let m, ts = translate_terms cfg m ts in
+            m, Why3.Term.t_app_infer s ts
+        | None ->
+            let m, tys, a = translate_fun_type cfg m !(s.sym_type) in
+            let id = Why3.Ident.id_fresh s.sym_name in
+            let f = Why3.Term.create_fsymbol id tys a in
+            if Logger.log_enabled() then
+              log "add psymbol %a : %a → %a" Why3.Pretty.print_ls f
+                (Debug.D.list Why3.Pretty.print_ty) tys
+                Why3.Pretty.print_ty a;
+            let m = {m with s2ls = (s,(f,false))::m.s2ls} in
+            let m, ts = translate_terms cfg m ts in
+            m, Why3.Term.t_app_infer f ts
+      end
+  | Vari x, ts ->
+      begin
+        match List.assoc_eq_opt Bindlib.eq_vars x m.v2vs with
+        | Some v ->
+            if ts = [] then m, Why3.Term.t_var v else raise Exit
+        | None ->
+            match List.assoc_eq_opt Bindlib.eq_vars x m.v2ls with
+            | Some(_, true) -> assert false
+            | Some(s, false) ->
+                let m, ts = translate_terms cfg m ts in
+                m, Why3.Term.t_app_infer s ts
+            | None -> assert false
+      end
+  | _ -> raise Exit
+
+and translate_terms cfg m ts =
+  List.fold_right
+    (fun t (m,ts) -> let m,t = translate_term cfg m t in m, t::ts)
+    ts (m,[])
+
+(** [translate_prop cfg m t] tries to translation a Lambdapi term [t:Prop] to
+    a Why3 proposition. *)
+let rec translate_prop : config -> l2y -> term -> l2y * Why3.Term.term =
+  let default m t =
+    try
+      let sym = List.assoc_eq (Eval.eq_modulo []) t m.t2ls in
+      (m, Why3.Term.ps_app sym [])
+    with Not_found ->
+      let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "X") [] in
+      if Logger.log_enabled() then
+        log "abstract [%a] as psymbol %a" term t Why3.Pretty.print_ls sym;
+      ({m with t2ls = (t,sym)::m.t2ls}, Why3.Term.ps_app sym [])
   in
+  fun cfg m t ->
+  if Logger.log_enabled() then log "translate_prop %a [%a]" l2y m term t;
   match get_args t with
-  | (Symb(s), [t]) when s == cfg.symb_P -> Some (translate_prop tbl ty_tbl t)
-  | _ -> None
+  | Symb s, [t1;t2] when s == cfg.symb_and ->
+      let m, t1 = translate_prop cfg m t1 in
+      let m, t2 = translate_prop cfg m t2 in
+      m, Why3.Term.t_and t1 t2
+  | Symb s, [t1;t2] when s == cfg.symb_or ->
+      let m, t1 = translate_prop cfg m t1 in
+      let m, t2 = translate_prop cfg m t2 in
+      m, Why3.Term.t_or t1 t2
+  | Symb s, [t1;t2] when s == cfg.symb_imp ->
+      let m, t1 = translate_prop cfg m t1 in
+      let m, t2 = translate_prop cfg m t2 in
+      m, Why3.Term.t_implies t1 t2
+  | Symb s, [t1;t2] when s == cfg.symb_eqv ->
+      let m, t1 = translate_prop cfg m t1 in
+      let m, t2 = translate_prop cfg m t2 in
+      m, Why3.Term.t_iff t1 t2
+  | Symb s, [t] when s == cfg.symb_not ->
+      let m, t = translate_prop cfg m t in
+      m, Why3.Term.t_not t
+  | Symb s, [] when s == cfg.symb_bot ->
+      m, Why3.Term.t_false
+  | Symb s, [] when s == cfg.symb_top ->
+      m, Why3.Term.t_true
+  | Symb s, [a;Abst(_,t)] when s == cfg.symb_ex ->
+      let m,a = translate_set m a
+      and x,t = Bindlib.unbind t in
+      let id = Why3.Ident.id_fresh (Bindlib.name_of x) in
+      let v = Why3.Term.create_vsymbol id a in
+      if Logger.log_enabled() then
+        log "add vsymbol %a" Why3.Pretty.print_vs v;
+      let m = {m with v2vs = (x,v)::m.v2vs} in
+      let m,t = translate_prop cfg m t in
+      (* remove x from m.v2vs ? *)
+      m, Why3.Term.t_exists_close [v] [] t
+  | Symb s, [a;Abst(_,t)] when s == cfg.symb_all ->
+      let m,a = translate_set m a
+      and x,t = Bindlib.unbind t in
+      let id = Why3.Ident.id_fresh (Bindlib.name_of x) in
+      let v = Why3.Term.create_vsymbol id a in
+      if Logger.log_enabled() then
+        log "add vsymbol %a" Why3.Pretty.print_vs v;
+      let m = {m with v2vs = (x,v)::m.v2vs} in
+      let m,t = translate_prop cfg m t in
+      (* remove x from m.v2vs ? *)
+      m, Why3.Term.t_forall_close [v] [] t
+  | Vari x, ts ->
+      begin
+        match List.assoc_eq_opt Bindlib.eq_vars x m.v2ls with
+        | Some(_, false) -> assert false
+        | Some(s, true) ->
+            begin
+              try
+                let m, ts = translate_terms cfg m ts in
+                m, Why3.Term.ps_app s ts
+              with Exit -> default m t
+            end
+        | None -> default m t
+      end
+  | Symb s, ts ->
+      begin
+        match List.assoc_eq_opt (==) s m.s2ls with
+        | Some(_, false) -> assert false
+        | Some(s, true) ->
+            begin
+              try
+                let m, ts = translate_terms cfg m ts in
+                m, Why3.Term.ps_app s ts
+              with Exit -> default m t
+            end
+        | None ->
+            begin
+              try
+                let m, tys = translate_pred_type cfg m !(s.sym_type) in
+                let id = Why3.Ident.id_fresh s.sym_name in
+                let f = Why3.Term.create_psymbol id tys in
+                if Logger.log_enabled() then
+                  log "add psymbol %a : %a" Why3.Pretty.print_ls f
+                    (Debug.D.list Why3.Pretty.print_ty) tys;
+                let m = {m with s2ls = (s,(f,true))::m.s2ls} in
+                let m, ts = translate_terms cfg m ts in
+                m, Why3.Term.ps_app f ts
+              with Exit -> default m t
+            end
+      end
+  | _ -> default m t
 
-(** [encode ss pos hs g] translates the hypotheses [hs] and the goal [g]
-    into Why3 terms, to construct a Why3 task. *)
-let encode : Sig_state.t -> Pos.popt -> Env.env -> term -> Why3.Task.task =
-  fun ss pos hs g ->
+(** [translate_goal ss pos env g] translates the hypotheses [env] and the goal
+    [g] into a Why3 task. *)
+let translate_goal :
+      Sig_state.t -> Pos.popt -> Env.env -> term -> Why3.Task.task =
+  fun ss pos env g ->
   let cfg = get_config ss pos in
-  let (constants, types, hypothesis) =
-    let translate_hyp (tbl,ty_tbl, map) (name, (_, hyp, _)) =
-      match translate_term cfg tbl ty_tbl (Bindlib.unbox hyp) with
-      | Some(tbl, ty_tbl, why3_hyp) ->
-        (tbl, ty_tbl, StrMap.add name why3_hyp map)
-      | None -> (tbl, ty_tbl , map)
-    in
-    List.fold_left translate_hyp ([], TyTable.empty, StrMap.empty) hs
-  in
-  (* Translate the goal term. *)
-  let (tbl, ty_tbl, why3_term) =
-    match translate_term cfg constants types g with
-    | Some(tbl, ty_tbl, why3_term) -> (tbl, ty_tbl, why3_term)
-    | None                         ->
-        fatal pos "The goal [%a] is not of the form [P _]" term g
+  (* Translate environment. *)
+  let translate_env_elt (name,(x,a,_)) (m,hyps) =
+    let a = Bindlib.unbox a in
+    (*if Logger.log_enabled() then log "translate_env_elt %a %a %s : %a"
+      l2y m Debug.D.(list (pair string Why3.Pretty.print_term)) hyps
+      name term a;*)
+    match get_args a with
+    | Symb s, [] when s == cfg.symb_Set -> (* type variable *)
+        let id = Why3.Ident.id_fresh name in
+        let tv = Why3.Ty.create_tvsymbol id in
+        if Logger.log_enabled() then
+          log "add tvsymbol %a" Why3.Pretty.print_tv tv;
+        {m with v2tv = (x,tv)::m.v2tv}, hyps
+    | Symb s, [t] when s == cfg.symb_T -> (* object *)
+        let m,t = translate_set m t in
+        let id = Why3.Ident.id_fresh name in
+        let f = Why3.Term.create_fsymbol id [] t in
+        if Logger.log_enabled() then
+          log "add fsymbol %a" Why3.Pretty.print_ls f;
+        {m with v2ls = (x,(f,false))::m.v2ls}, hyps
+    | Symb s, [t] when s == cfg.symb_P -> (* assumption *)
+        let m,t = translate_prop cfg m t in
+        m, (name,t)::hyps
+    | _ -> (* predicate symbol *)
+        let m, tys = translate_pred_type cfg m a in
+        let id = Why3.Ident.id_fresh name in
+        let f = Why3.Term.create_psymbol id tys in
+        if Logger.log_enabled() then
+          log "add psymbol %a" Why3.Pretty.print_ls f;
+        {m with v2ls = (x,(f,true))::m.v2ls}, hyps
   in
-  (* Add the declaration of every constant in a task. *)
-  let fn tsk (_,t) = Why3.Task.add_param_decl tsk t in
-  let tsk = List.fold_left fn None tbl in
-  (* Same for types. *)
-  let tsk =
-    let do_sym tsk _ tys = Why3.Task.add_ty_decl tsk tys in
-    let do_var tsk _ _ = tsk in
-    TyTable.fold_left ~do_var ~do_sym tsk ty_tbl
+  let translate_env_elt b m = try translate_env_elt b m with Exit -> m in
+  let m, hyps = List.fold_right translate_env_elt env (empty_l2y, []) in
+  if Logger.log_enabled() then log "hyps: %a"
+    Debug.D.(list (pair string Why3.Pretty.print_term)) hyps;
+  (* Translate the goal. *)
+  let m, g =
+    match get_args g with
+    | Symb s, [t] when s == cfg.symb_P ->
+        begin
+          try translate_prop cfg m t
+          with Exit -> fatal pos "The goal cannot be translated to Why3."
+        end
+    | _ -> fatal pos "The goal is not of the form [%a _]." sym cfg.symb_P
   in
-  (* Add the declaration of every hypothesis in the task. *)
-  let fn name t tsk =
+  if Logger.log_enabled() then log "goal: %a" Why3.Pretty.print_term g;
+  if Logger.log_enabled() then log "map: %a" l2y m;
+  (* Build the task. *)
+  let tsk = None in
+  (* Add the declarations of type symbols. *)
+  let add_s2ts_decl tsk (_,tsym) = Why3.Task.add_ty_decl tsk tsym in
+  let tsk = List.fold_left add_s2ts_decl tsk m.s2ts in
+  let add_t2ts_decl tsk (_,tsym) = Why3.Task.add_ty_decl tsk tsym in
+  let tsk = List.fold_left add_t2ts_decl tsk m.t2ts in
+  if Logger.log_enabled() then log "%a" Why3.Pretty.print_task tsk;
+  (* Add the declarations of term symbols. *)
+  let add_s2ls_decl tsk (_,(lsym,_)) = Why3.Task.add_param_decl tsk lsym in
+  let tsk = List.fold_left add_s2ls_decl tsk m.s2ls in
+  let add_v2ls_decl tsk (_,(lsym,_)) = Why3.Task.add_param_decl tsk lsym in
+  let tsk = List.fold_left add_v2ls_decl tsk m.v2ls in
+  let add_t2ls_decl tsk (_,lsym) = Why3.Task.add_param_decl tsk lsym in
+  let tsk = List.fold_left add_t2ls_decl tsk m.t2ls in
+  (* Add the declarations of assumptions. *)
+  let add_hyp_decl tsk (name,prop) =
     let axiom = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh name) in
-    Why3.Task.add_prop_decl tsk Why3.Decl.Paxiom axiom t
+    Why3.Task.add_prop_decl tsk Why3.Decl.Paxiom axiom prop
   in
-  let tsk = StrMap.fold fn hypothesis tsk in
-  (* Add the goal itself. *)
-  let goal = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "main_goal") in
-  (* Return the task that contains the encoded lambdapi formula in Why3. *)
-  Why3.Task.add_prop_decl tsk Why3.Decl.Pgoal goal why3_term
-
-(** [run_task tsk pos prover_name] Run the task [tsk] with the specified
-    prover named [prover_name] and return the answer of the prover. *)
-let run_task : Why3.Task.task -> Pos.popt -> string -> bool =
+  let tsk = List.fold_left add_hyp_decl tsk hyps in
+  (* Add the goal. *)
+  let goal = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "G") in
+  let tsk = Why3.Task.add_prop_decl tsk Why3.Decl.Pgoal goal g in
+  if Logger.log_enabled() then log "%a" Why3.Pretty.print_task tsk;
+  tsk
+
+(** [run tsk pos prover_name] sends [tsk] to [prover_name]. *)
+let run : Why3.Task.task -> Pos.popt -> string -> bool =
   fun tsk pos prover_name ->
   (* Filter the set of why3 provers. *)
   let filter = Why3.Whyconf.parse_filter_prover prover_name in
@@ -203,25 +390,26 @@ let run_task : Why3.Task.task -> Pos.popt -> string -> bool =
   (* Fail if we did not find a matching prover. *)
   if Why3.Whyconf.Mprover.is_empty provers then
     begin
-      fatal_msg "prover \"%s\" not found.@." prover_name;
-      let provers = Why3.Whyconf.get_provers why3_config in
-      let _ =
-        if Why3.Whyconf.Mprover.is_empty provers then
-          fatal_msg "There are no available Why3 provers.@."
-        else
-          let fn p _ = fatal_msg " - %a@." Why3.Whyconf.print_prover p in
-          fatal_msg "The available Why3 provers are:@.";
-          Why3.Whyconf.Mprover.iter fn provers
-      in
-      fatal_msg "Why3 configuration read from \"%s\".@."
+      fatal_msg "Your prover might not be installed or detected.\n";
+      fatal_msg "Remember to run \"why3 config detect\" \
+                 after installing a prover.";
+      fatal_msg "Why3 configuration read from \"%s\".\n"
         (Why3.Whyconf.get_conf_file why3_config);
-      fatal_msg "Your prover might not be installed or detected, ";
-      fatal pos "remember to run [why3 config detect]."
+      let provers = Why3.Whyconf.get_provers why3_config in
+      if Why3.Whyconf.Mprover.is_empty provers then
+        fatal_msg "There are no available provers.@."
+      else
+        begin
+          fatal_msg "The available provers are:@.";
+          let f p _ = fatal_msg " - %a@." Why3.Whyconf.print_prover p in
+          Why3.Whyconf.Mprover.iter f provers
+        end;
+      fatal pos "prover \"%s\" not found.@." prover_name;
     end;
   (* Return the prover configuration and load the driver. *)
   let prover = snd (Why3.Whyconf.Mprover.max_binding provers) in
   let driver =
-    try Why3.Driver.(load_driver_for_prover why3_main why3_env prover)
+    try Why3.Driver.load_driver_for_prover why3_main why3_env prover
     with e -> fatal pos "Failed to load driver for \"%s\": %a"
                 prover.prover.prover_name Why3.Exn_printer.exn_printer e
   in
@@ -237,14 +425,16 @@ let run_task : Why3.Task.task -> Pos.popt -> string -> bool =
     [prover_name] (if given or a default one otherwise) on the goal type [gt],
     and fails if no proof is found. *)
 let handle :
-  Sig_state.t -> Pos.popt -> string option -> Proof.goal_typ -> unit =
-  fun ss pos prover_name {goal_meta = _; goal_hyps = hyps; goal_type = trm} ->
+  Sig_state.t -> Pos.popt -> string option -> goal_typ -> unit =
+  fun ss pos prover_name
+      ({goal_meta = _; goal_hyps = hyps; goal_type = t} as gt) ->
+  let g = Typ gt in
+  if Logger.log_enabled() then log "%a%a" Goal.hyps g Goal.pp g;
+  (* Encode the goal in Why3. *)
+  let tsk = translate_goal ss pos hyps t in
   (* Get the name of the prover. *)
   let prover_name = Option.get !default_prover prover_name in
-  if Logger.log_enabled () then
-    log_why3 "running with prover \"%s\"" prover_name;
-  (* Encode the goal in Why3. *)
-  let tsk = encode ss pos hyps trm in
+  if Logger.log_enabled() then log "running with prover \"%s\"" prover_name;
   (* Run the task with the prover named [prover_name]. *)
-  if not (run_task tsk pos prover_name) then
+  if not (run tsk pos prover_name) then
     fatal pos "\"%s\" did not find a proof" prover_name
diff --git a/src/lplib/base.ml b/src/lplib/base.ml
index b64ceff68..56dc3a358 100644
--- a/src/lplib/base.ml
+++ b/src/lplib/base.ml
@@ -18,6 +18,7 @@ let (|+) p1 p2 : 'a pp = fun ppf arg -> (p1 ++ p2) ppf ((), arg)
 let (+|) p1 p2 : 'a pp = fun ppf arg -> (p1 ++ p2) ppf (arg, ())
 
 let int : int pp = Format.pp_print_int
+let char : char pp = Format.pp_print_char
 let string : string pp = Format.pp_print_string
 let float : float pp = fun ppf -> out ppf "%f"
 let unit : unit outfmt -> unit pp = fun fmt ppf () -> out ppf fmt
diff --git a/src/lplib/list.ml b/src/lplib/list.ml
index dd3af5391..2fd3d9cfb 100644
--- a/src/lplib/list.ml
+++ b/src/lplib/list.ml
@@ -139,6 +139,8 @@ let assoc_eq : 'a eq -> 'a -> ('a * 'b) list -> 'b = fun eq k ->
     | _ :: t -> loop t
   in loop
 
+let assoc_eq_opt eq x l = try Some (assoc_eq eq x l) with Not_found -> None
+
 (** [remove_phys_dups l] uniqify list [l] keeping only the last element, using
     physical equality. *)
 let rec remove_phys_dups : 'a list -> 'a list = function
diff --git a/tests/OK/logic.lp b/tests/OK/logic.lp
index 35211f932..4a40a82a2 100644
--- a/tests/OK/logic.lp
+++ b/tests/OK/logic.lp
@@ -117,3 +117,6 @@ builtin "not"   ≔ not;
 constant symbol ex: Π (a : U), (T a → Prop) → Prop;
 builtin "ex" ≔ ex; 
 builtin "all" ≔ all;
+
+symbol eqv p q ≔ {|and|} (imp p q) (imp q p);
+builtin "eqv" ≔ eqv;
diff --git a/tests/OK/why3.lp b/tests/OK/why3.lp
index 52ca75d0f..23a34e44c 100644
--- a/tests/OK/why3.lp
+++ b/tests/OK/why3.lp
@@ -14,7 +14,6 @@ opaque symbol thm_and1 : Π (a b : Prop), P ({|and|} a b) → P a
     why3;
 end;
 
-
 opaque symbol thm_and2 : Π (a b : Prop), P ({|and|} a b) → P b
 ≔ begin
     why3;
@@ -39,3 +38,24 @@ opaque symbol thm_imp : Π (a b : Prop), P (imp a b) → P a → P b
 ≔ begin
     why3;
 end;
+
+symbol o : U;
+rule T o ↪ Prop;
+
+constant symbol nat: U;
+symbol even (_: T nat): Prop;
+
+/*opaque symbol thm_ex : P (ex o (λ p: T o, imp p p))
+≔ begin 
+  why3;
+end;*/
+
+opaque symbol thm_even : P (ex nat (λ n: T nat, imp (even n) (even n)))
+≔ begin
+  why3;
+end;
+
+opaque symbol tyvar (a: U) (q: T a → T o): P (ex a (λ n: T a, imp (q n) (q n)))
+≔ begin
+  why3;
+end; 
diff --git a/tests/OK/why3_quantifiers.lp b/tests/OK/why3_quantifiers.lp
deleted file mode 100644
index 116cbbad2..000000000
--- a/tests/OK/why3_quantifiers.lp
+++ /dev/null
@@ -1,30 +0,0 @@
-require open tests.OK.logic;
-require open tests.OK.natural;
-
-prover "Alt-Ergo";
-prover_timeout 2;
-
-symbol o : U;
-rule T o ↪ Prop;
-
-constant symbol nat: U;
-symbol even (_: T nat): Prop;
-
-// Test a quantification on the boolean type
-opaque symbol thm_ex : P (ex o (λ p: T o, imp p p))
-≔ begin 
-  why3; 
-end;
-
-// Quantification on a type symbol
-opaque symbol thm_even : P (ex nat (λ n: T nat, imp (even n) (even n)))
-≔ begin
-  why3;
-end;
-
-// Quantification on a type variable
-opaque symbol tyvar (a: U) (q: T a → T o): P (ex a (λ n: T a, imp (q n) (q n)))
-≔ begin
-  why3;
-end; 
-