diff --git a/main.ml b/main.ml
index 31bc94e..ef7c7ef 100644
--- a/main.ml
+++ b/main.ml
@@ -157,8 +157,10 @@ while !subgoals <> [] do
 done;
 
 let finalLam = !fill_holes [] in
-    if (typecheck [] finalLam ty) then
-        Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
+    if (typecheck [] finalLam ty) then (
+        Printf.printf "Final proof :\n";
+        reduce finalLam
+    )
     else (
         Printf.printf "Invalid proof constructed!\n";
         Printf.printf "%s can't be typed with %s.\n" (string_of_lam finalLam) (string_of_ty ty);
diff --git a/pieuvre.ml b/pieuvre.ml
index 2cc64ba..f26cea5 100644
--- a/pieuvre.ml
+++ b/pieuvre.ml
@@ -90,7 +90,7 @@ let rec alpha (l1: lam) (l2: lam) : bool =
 
 (* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
 let rec betastep (l: lam) : lam option = match l with
-    | LFun(v,t,l') -> betastep l'
+    | LFun(v,t,l') -> Option.bind (betastep l') (fun l' -> Some (LFun(v,t,l')))
     | LApp(lf,lx) ->
         begin
         match (betastep lf) with
@@ -104,7 +104,7 @@ let rec betastep (l: lam) : lam option = match l with
                 | _ -> None (* On ne peut pas β-réduire *)
         end
     | LVar(x) -> None
-    | LExf(l',_) -> betastep l'
+    | LExf(l',t) -> Option.bind (betastep l') (fun l' -> Some (LExf(l',t)))
 ;;
 
 (* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
diff --git a/tests/cut-impl.8pus b/tests/cut-impl.8pus
new file mode 100644
index 0000000..b0ede74
--- /dev/null
+++ b/tests/cut-impl.8pus
@@ -0,0 +1,10 @@
+(A -> B -> C) -> (B -> A -> C)
+intro f.
+intro b.
+intro a.
+cut (B -> C).
+intro bc.
+apply bc.
+assumption.
+apply f.
+assumption.