diff --git a/src/backend/coq.ml b/src/backend/coq.ml
index 39009c2a..35ff1ab9 100644
--- a/src/backend/coq.ml
+++ b/src/backend/coq.ml
@@ -32,6 +32,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     end)
 
   let name c = c.S.St.name
+  let name_tmp c = c.S.St.name ^ "_or"
 
   let pp_atom fmt a =
     if a == S.St.(a.var.pa) then
@@ -63,7 +64,9 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     Format.fprintf fmt "@].@\n";
     m
 
-  let clausify 
+  let clausify fmt clause =
+    Format.fprintf fmt "assert (%s: %a).@\nintros; try destruct %s; auto. clear %s.@\n"
+      (name clause) pp_clause clause (name_tmp clause) (name_tmp clause)
 
   let elim_duplicate fmt goal hyp _ =
     (** Printing info comment in coq *)
@@ -94,7 +97,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     Format.fprintf fmt "exact (%s%a).@\n"
       (name h1) (fun fmt -> Array.iter (fun b ->
           if b == a then begin
-            Format.fprintf fmt " (fun p => %s%a"
+            Format.fprintf fmt " (fun p => %s%a)"
               (name h2) (fun fmt -> (Array.iter (fun c ->
                   if c == a.S.St.neg then
                     Format.fprintf fmt " (fun np => np p)"
@@ -110,11 +113,14 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     let clause = node.S.conclusion in
     match node.S.step with
     | S.Hypothesis ->
-      A.prove_hyp fmt (name clause) clause
+      A.prove_hyp fmt (name_tmp clause) clause;
+      clausify fmt clause
     | S.Assumption ->
-      A.prove_assumption fmt (name clause) clause
+      A.prove_assumption fmt (name_tmp clause) clause;
+      clausify fmt clause
     | S.Lemma _ ->
-      A.prove_lemma fmt (name clause) clause
+      A.prove_lemma fmt (name_tmp clause) clause;
+      clausify fmt clause
     | S.Duplicate (p, l) ->
       let c = (S.expand p).S.conclusion in
       elim_duplicate fmt clause c l
@@ -130,7 +136,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     let aux () node =
       Format.fprintf fmt "%a@\n@\n" (prove_node h) node
     in
-    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
+    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n@\n";
     S.fold aux () p
 
 end