diff git a/examples/bts/231_destruct/why3session.xml b/examples/bts/231_destruct/why3session.xml
index 26ca725e66acd242dc965ccdf76f13ce1c27df4b..1c8491e8d5ff443710c8a5288f72857942c86f25 100644
 a/examples/bts/231_destruct/why3session.xml
+++ b/examples/bts/231_destruct/why3session.xml
@@ 52,19 +52,23 @@
+
+
+
+
+
+
+
+
+
+








+
+
@@ 141,29 +145,5 @@
























diff git a/examples/bts/231_destruct/why3shapes.gz b/examples/bts/231_destruct/why3shapes.gz
index 7c833ebc3d6777a168e784f90a00517b9e71ee75..d956b26bf7a37bd423cdbfae680ee9a00633d4ed 100644
Binary files a/examples/bts/231_destruct/why3shapes.gz and b/examples/bts/231_destruct/why3shapes.gz differ
diff git a/src/transform/destruct.ml b/src/transform/destruct.ml
index 9872abaa98109873a5a1c51cadc5e2bafb209c3b..f591c97964e0f95723c04df012a2bf8f3799704e 100644
 a/src/transform/destruct.ml
+++ b/src/transform/destruct.ml
@@ 149,24 +149,22 @@ let destruct_term ~recursive (t: term) =
l.ls_constr <> 0
in
 (* Check if a new goal is created in the branch *)
 let contains_goal l =
 List.exists (fun x > match x with  Goal_term _ > true  _ > false) l
 in

 (* Main function *)
 let rec destruct_term (t: term) =
 let destruct_term_exception t =
+ (* Main recursive function:
+ [toplevel] when true, removing implications is allowed. Become false as
+ soon as we destruct nonimplication construct
+ *)
+ let rec destruct_term ~toplevel (t: term) =
+ let destruct_term_exception ~toplevel t =
if not recursive then [[Axiom_term t]] else
 match destruct_term t with
+ match destruct_term ~toplevel t with
 exception _ > [[Axiom_term t]]
 l > l
in
match t.t_node with
 Tbinop (Tand, t1, t2) >
 let l1 = destruct_term_exception t1 in
 let l2 = destruct_term_exception t2 in
+ let l1 = destruct_term_exception ~toplevel:false t1 in
+ let l2 = destruct_term_exception ~toplevel:false t2 in
(* For each parallel branch of l1 we have to append *all* parallel
branch of l2 which are not new goals. In case of new goals, we are
not allowed to use the left/right conclusions to prove the goal.
@@ 177,25 +175,19 @@ let destruct_term ~recursive (t: term) =
(* TODO efficiency: this is not expected to work on very large terms
with tons of Tand/Tor. *)
List.fold_left (fun par_acc seq_list1 >
 if contains_goal seq_list1 then
 par_acc @ [seq_list1]
 else
 List.fold_left (fun par_acc seq_list2 >
 if contains_goal seq_list2 then
 par_acc @ [seq_list2]
 else
 par_acc @ [seq_list1 @ seq_list2]) par_acc l2
+ List.fold_left (fun par_acc seq_list2 >
+ par_acc @ [seq_list1 @ seq_list2]) par_acc l2
) [] l1
 Tbinop (Tor, t1, t2) >
 let l1 = destruct_term_exception t1 in
 let l2 = destruct_term_exception t2 in
+ let l1 = destruct_term_exception ~toplevel:false t1 in
+ let l2 = destruct_term_exception ~toplevel:false t2 in
(* The two branch are completely disjoint. We just concatenate them to
ensure they are done in parallel *)
l1 @ l2
  Tbinop (Timplies, t1, t2) >
+  Tbinop (Timplies, t1, t2) when toplevel >
(* The premises is converted to a goal. The rest is recursively
destructed in parallel. *)
 let l2 = destruct_term_exception t2 in
+ let l2 = destruct_term_exception ~toplevel t2 in
[Goal_term t1] :: l2
 Tquant (Texists, tb) >
let (vsl, tr, te) = Term.t_open_quant tb in
@@ 209,7 +201,7 @@ let destruct_term ~recursive (t: term) =
let new_t = t_quant_close Texists tl tr part_t in
(* The recursive call is done after new symbols are introduced so we
readd the new decls to every generated list. *)
 let l_t = destruct_term_exception new_t in
+ let l_t = destruct_term_exception ~toplevel:false new_t in
List.map (fun x > Param x_decl :: x) l_t
with
 Ty.TypeMismatch (ty1, ty2) >
@@ 237,7 +229,7 @@ let destruct_term ~recursive (t: term) =
 Tnot {t_node = Tapp (ls,
[{t_node = Tapp (cs1, _); _}; {t_node = Tapp (cs2, _); _}]); _}
when ls_equal ls ps_equ && is_constructor cs1 && is_constructor cs2 >
 (* Cs1 [l1] <> Cs2 [l2] *)
+ (* Cs1 [l1] = Cs2 [l2] *)
if ls_equal cs1 cs2 then
[[Axiom_term t]]
else
@@ 245,7 +237,7 @@ let destruct_term ~recursive (t: term) =
[[]]
 _ > raise (Arg_trans ("destruct"))
in
 destruct_term t
+ destruct_term ~toplevel:true t
(* Destruct the head term of an hypothesis if it is either
conjunction, disjunction or exists *)