diff --git a/channel/heap_lang.v b/channel/heap_lang.v
index d3bd5559279ba8abfd586022da0a73a343f9cc51..9d8ecbb6c089d902b0a4aa8c68ec62349d0af4e2 100644
--- a/channel/heap_lang.v
+++ b/channel/heap_lang.v
@@ -181,12 +181,7 @@ Qed.
 Lemma fill_not_value e K :
   e2v e = None -> e2v (fill K e) = None.
 Proof.
-  intros Hnval.  induction K =>/=; try reflexivity.
-  - done.
-  - by rewrite IHK /=.
-  - by rewrite v2v /= IHK /=.
-  - by rewrite IHK /=.
-  - by rewrite IHK /=.
+  intros Hnval.  induction K =>/=; by rewrite ?v2v /= ?IHK /=.
 Qed.
 
 Lemma fill_not_value2 e K v :