really fix build

theories/typing/naive_simpl.v

@@ -302,7 +302,7 @@ Ltac naive_simpl_go :=
           match P with
           | ∃ _, _ => case
           | _ = _ => let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi
-          | _ => check_hyp_not_exists P; intros ?; subst
+          | _ => assert_is_not_trivial P; intros ?; subst
           | _ => move => _
           end
         end]