1 files changed, 3 insertions, 6 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 5a61a9c..713a373 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -350,13 +350,10 @@ Proof.
   econstructor; simpl; trivial.
   intros.
   inv_incr.
-  assert (st_controllogic s8 = st_controllogic s2).
-  { rewrite <- H5. rewrite <- H6. rewrite <- H7. trivial. }
+  assert (st_controllogic s8 = st_controllogic s2) by congruence.
   rewrite <- H10.
-  assert (st_datapath s8 = st_datapath s2).
-  { rewrite <- EQ4. rewrite <- EQ3. rewrite <- EQ2. trivial. }
-  assert (st_st s5 = st_st s2).
-  { rewrite H10. rewrite <- H50. trivial. }
+  assert (st_datapath s8 = st_datapath s2) by congruence.
+  assert (st_st s5 = st_st s2) by congruence.
   rewrite H80. rewrite H81. rewrite H82.
   eauto with htlspec.
 Qed.