diff --git a/theories/type_systems/systemf/church_encodings_faithful.v b/theories/type_systems/systemf/church_encodings_faithful.v
index d28a947df307e63229f536e7502eb0a17c2120f0..4620898fb63b128a428a8faace9621f86201febb 100644
--- a/theories/type_systems/systemf/church_encodings_faithful.v
+++ b/theories/type_systems/systemf/church_encodings_faithful.v
@@ -265,9 +265,9 @@ Proof.
     + simpl. bs_step_det.
       rewrite subst_is_closed_nil; first by apply big_step_of_val.
       apply sem_type_closed_val in Ha12. naive_solver.
-    + simp type_interp.
+    + by simp type_interp.
   - simp type_interp. exists b1, b2. split_and!.
     + by apply big_step_of_val.
     + simpl. bs_step_det. by apply big_step_of_val.
-    + simp type_interp.
+    + by simp type_interp.
 Qed.