diff --git a/src/ecMatching.ml b/src/ecMatching.ml
index 1d1b45521..c0cadee04 100644
--- a/src/ecMatching.ml
+++ b/src/ecMatching.ml
@@ -405,8 +405,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
 
     let var_form_match ((x, xty) : ident * ty) (f : form) =
       match EV.get x !ev.evm_form with
-      | None ->
-        failure ()
+      | None -> assert false
 
       | Some `Unset ->
         let f = norm f in
diff --git a/tests/split.ec b/tests/split.ec
index f440dfd52..96db6d2db 100644
--- a/tests/split.ec
+++ b/tests/split.ec
@@ -3,33 +3,13 @@ require import AllCore.
 
 print andWr.
 
-lemma test : forall a b c d e f, a && b /\ c && d /\ e /\ f.
+lemma test : forall a b c d e f,
+    a && b /\ c && d  =>
+    e /\ f =>
+    a && b /\ c && d /\ e /\ f.
 proof.
 move=> *.
-
-split 5.
-split.
-admit.
-
-
-
-gl = a && b
-gr = c /\ d
-
-proja2 gl = b
-
-conja (proja1 gl) (conj (proja2 gl) gr) = a && (b /\ (c /\ d))
-
-
-
-admit.
-
-
-
-admit.
-
-
-
-
-abort.
-
+split 3.
+assumption.
+assumption.
+qed.