Update SpecificGen to be faster

12 files changed, 138 insertions, 36 deletions

diff --git a/src/SpecificGen/GF2213_32BoundedCommon.v b/src/SpecificGen/GF2213_32BoundedCommon.v
index df3f4739e..8caf225aa 100644
--- a/src/SpecificGen/GF2213_32BoundedCommon.v
+++ b/src/SpecificGen/GF2213_32BoundedCommon.v
@@ -289,15 +289,29 @@ Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW
       app_wire_digitsW x (Tuple.map word64ize).
 
 (** TODO: Turn this into a lemma to speed up proofs *)
+Ltac unfold_is_bounded_in' H :=
+  lazymatch type of H with
+  | andb _ _ = true
+    => apply andb_prop in H;
+       let H1 := fresh in
+       let H2 := fresh in
+       destruct H as [H1 H2];
+       unfold_is_bounded_in' H1;
+       unfold_is_bounded_in' H2
+  | _ => idtac
+  end.
 Ltac unfold_is_bounded_in H :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2213_32WToZ, wire_digitsWToZ in H;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2213_32 List.length wire_widths] in H;
-  rewrite ?Bool.andb_true_iff in H.
+  unfold_is_bounded_in' H.
 
 Ltac unfold_is_bounded :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2213_32WToZ, wire_digitsWToZ;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2213_32 List.length wire_widths];
-  rewrite ?Bool.andb_true_iff.
+  repeat match goal with
+         | [ |- andb _ _ = true ] => apply andb_true_intro
+         | [ |- and _ _ ] => split
+         end.
 
 Local Transparent bit_width.
 Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width.
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index ff4999bcc..0414d2188 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -352,12 +352,14 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe2213_32WToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- wire_digitsWToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
+  cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *;
+  destruct_head' prod;
   change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
@@ -367,11 +369,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe2213_32WToZ; simpl @wire_digitsWToZ;
-  unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
   change WordW.wordWToZ with word64ToZ in *;
-  repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
+  unfold_is_bounded;
+  Z.ltb_to_lt;
+  try omega; try reflexivity.
 
 
 Ltac rexpr_correct :=
diff --git a/src/SpecificGen/GF2519_32BoundedCommon.v b/src/SpecificGen/GF2519_32BoundedCommon.v
index cea3e4f10..998dd899d 100644
--- a/src/SpecificGen/GF2519_32BoundedCommon.v
+++ b/src/SpecificGen/GF2519_32BoundedCommon.v
@@ -289,15 +289,29 @@ Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW
       app_wire_digitsW x (Tuple.map word64ize).
 
 (** TODO: Turn this into a lemma to speed up proofs *)
+Ltac unfold_is_bounded_in' H :=
+  lazymatch type of H with
+  | andb _ _ = true
+    => apply andb_prop in H;
+       let H1 := fresh in
+       let H2 := fresh in
+       destruct H as [H1 H2];
+       unfold_is_bounded_in' H1;
+       unfold_is_bounded_in' H2
+  | _ => idtac
+  end.
 Ltac unfold_is_bounded_in H :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2519_32WToZ, wire_digitsWToZ in H;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2519_32 List.length wire_widths] in H;
-  rewrite ?Bool.andb_true_iff in H.
+  unfold_is_bounded_in' H.
 
 Ltac unfold_is_bounded :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2519_32WToZ, wire_digitsWToZ;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2519_32 List.length wire_widths];
-  rewrite ?Bool.andb_true_iff.
+  repeat match goal with
+         | [ |- andb _ _ = true ] => apply andb_true_intro
+         | [ |- and _ _ ] => split
+         end.
 
 Local Transparent bit_width.
 Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width.
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index aac5d8fb9..d2e349bd6 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -352,12 +352,14 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe2519_32WToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- wire_digitsWToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
+  cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *;
+  destruct_head' prod;
   change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
@@ -367,11 +369,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe2519_32WToZ; simpl @wire_digitsWToZ;
-  unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
   change WordW.wordWToZ with word64ToZ in *;
-  repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
+  unfold_is_bounded;
+  Z.ltb_to_lt;
+  try omega; try reflexivity.
 
 
 Ltac rexpr_correct :=
diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v
index f88b8a152..4c186fd26 100644
--- a/src/SpecificGen/GF25519_32BoundedCommon.v
+++ b/src/SpecificGen/GF25519_32BoundedCommon.v
@@ -289,15 +289,29 @@ Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW
       app_wire_digitsW x (Tuple.map word64ize).
 
 (** TODO: Turn this into a lemma to speed up proofs *)
+Ltac unfold_is_bounded_in' H :=
+  lazymatch type of H with
+  | andb _ _ = true
+    => apply andb_prop in H;
+       let H1 := fresh in
+       let H2 := fresh in
+       destruct H as [H1 H2];
+       unfold_is_bounded_in' H1;
+       unfold_is_bounded_in' H2
+  | _ => idtac
+  end.
 Ltac unfold_is_bounded_in H :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_32WToZ, wire_digitsWToZ in H;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_32 List.length wire_widths] in H;
-  rewrite ?Bool.andb_true_iff in H.
+  unfold_is_bounded_in' H.
 
 Ltac unfold_is_bounded :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_32WToZ, wire_digitsWToZ;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_32 List.length wire_widths];
-  rewrite ?Bool.andb_true_iff.
+  repeat match goal with
+         | [ |- andb _ _ = true ] => apply andb_true_intro
+         | [ |- and _ _ ] => split
+         end.
 
 Local Transparent bit_width.
 Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width.
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index 96958f330..f1b476717 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -352,12 +352,14 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe25519_32WToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- wire_digitsWToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
+  cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *;
+  destruct_head' prod;
   change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
@@ -367,11 +369,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe25519_32WToZ; simpl @wire_digitsWToZ;
-  unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
   change WordW.wordWToZ with word64ToZ in *;
-  repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
+  unfold_is_bounded;
+  Z.ltb_to_lt;
+  try omega; try reflexivity.
 
 
 Ltac rexpr_correct :=
diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v
index b14612f07..d1e3c6407 100644
--- a/src/SpecificGen/GF25519_64BoundedCommon.v
+++ b/src/SpecificGen/GF25519_64BoundedCommon.v
@@ -289,15 +289,29 @@ Definition wire_digitsW_word128ize (x : wire_digitsW) : wire_digitsW
       app_wire_digitsW x (Tuple.map word128ize).
 
 (** TODO: Turn this into a lemma to speed up proofs *)
+Ltac unfold_is_bounded_in' H :=
+  lazymatch type of H with
+  | andb _ _ = true
+    => apply andb_prop in H;
+       let H1 := fresh in
+       let H2 := fresh in
+       destruct H as [H1 H2];
+       unfold_is_bounded_in' H1;
+       unfold_is_bounded_in' H2
+  | _ => idtac
+  end.
 Ltac unfold_is_bounded_in H :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_64WToZ, wire_digitsWToZ in H;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_64 List.length wire_widths] in H;
-  rewrite ?Bool.andb_true_iff in H.
+  unfold_is_bounded_in' H.
 
 Ltac unfold_is_bounded :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_64WToZ, wire_digitsWToZ;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_64 List.length wire_widths];
-  rewrite ?Bool.andb_true_iff.
+  repeat match goal with
+         | [ |- andb _ _ = true ] => apply andb_true_intro
+         | [ |- and _ _ ] => split
+         end.
 
 Local Transparent bit_width.
 Definition Pow2_128 := Eval compute in 2^Z.of_nat bit_width.
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index 0811a71cc..3056569bd 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -352,12 +352,14 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe25519_64WToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- wire_digitsWToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
+  cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *;
+  destruct_head' prod;
   change word128ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
@@ -367,11 +369,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe25519_64WToZ; simpl @wire_digitsWToZ;
-  unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
   change WordW.wordWToZ with word128ToZ in *;
-  repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
+  unfold_is_bounded;
+  Z.ltb_to_lt;
+  try omega; try reflexivity.
 
 
 Ltac rexpr_correct :=
diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v
index 2f87412c9..fec786e23 100644
--- a/src/SpecificGen/GF41417_32BoundedCommon.v
+++ b/src/SpecificGen/GF41417_32BoundedCommon.v
@@ -289,15 +289,29 @@ Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW
       app_wire_digitsW x (Tuple.map word64ize).
 
 (** TODO: Turn this into a lemma to speed up proofs *)
+Ltac unfold_is_bounded_in' H :=
+  lazymatch type of H with
+  | andb _ _ = true
+    => apply andb_prop in H;
+       let H1 := fresh in
+       let H2 := fresh in
+       destruct H as [H1 H2];
+       unfold_is_bounded_in' H1;
+       unfold_is_bounded_in' H2
+  | _ => idtac
+  end.
 Ltac unfold_is_bounded_in H :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe41417_32WToZ, wire_digitsWToZ in H;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths] in H;
-  rewrite ?Bool.andb_true_iff in H.
+  unfold_is_bounded_in' H.
 
 Ltac unfold_is_bounded :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe41417_32WToZ, wire_digitsWToZ;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths];
-  rewrite ?Bool.andb_true_iff.
+  repeat match goal with
+         | [ |- andb _ _ = true ] => apply andb_true_intro
+         | [ |- and _ _ ] => split
+         end.
 
 Local Transparent bit_width.
 Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width.
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index 68de90117..dcf396580 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -352,12 +352,14 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe41417_32WToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- wire_digitsWToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
+  cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *;
+  destruct_head' prod;
   change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
@@ -367,11 +369,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe41417_32WToZ; simpl @wire_digitsWToZ;
-  unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
   change WordW.wordWToZ with word64ToZ in *;
-  repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
+  unfold_is_bounded;
+  Z.ltb_to_lt;
+  try omega; try reflexivity.
 
 
 Ltac rexpr_correct :=
diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v
index bd2394540..911fdb5ba 100644
--- a/src/SpecificGen/GF5211_32BoundedCommon.v
+++ b/src/SpecificGen/GF5211_32BoundedCommon.v
@@ -289,15 +289,29 @@ Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW
       app_wire_digitsW x (Tuple.map word64ize).
 
 (** TODO: Turn this into a lemma to speed up proofs *)
+Ltac unfold_is_bounded_in' H :=
+  lazymatch type of H with
+  | andb _ _ = true
+    => apply andb_prop in H;
+       let H1 := fresh in
+       let H2 := fresh in
+       destruct H as [H1 H2];
+       unfold_is_bounded_in' H1;
+       unfold_is_bounded_in' H2
+  | _ => idtac
+  end.
 Ltac unfold_is_bounded_in H :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe5211_32WToZ, wire_digitsWToZ in H;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths] in H;
-  rewrite ?Bool.andb_true_iff in H.
+  unfold_is_bounded_in' H.
 
 Ltac unfold_is_bounded :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe5211_32WToZ, wire_digitsWToZ;
   cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths];
-  rewrite ?Bool.andb_true_iff.
+  repeat match goal with
+         | [ |- andb _ _ = true ] => apply andb_true_intro
+         | [ |- and _ _ ] => split
+         end.
 
 Local Transparent bit_width.
 Definition Pow2_64 := Eval compute in 2^Z.of_nat bit_width.
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index ec776afd9..69382ec40 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -352,12 +352,14 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
          Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   match goal with
   | [ |- fe5211_32WToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- wire_digitsWToZ ?x = _ /\ _ ]
-    => destruct x; destruct_head_hnf' prod
+    => generalize dependent x; intros
   | [ |- _ = _ ]
     => exact Hbounds_left
   end;
+  cbv [interp_flat_type WordW.interp_base_type remove_all_binders] in *;
+  destruct_head' prod;
   change word64ToZ with WordW.wordWToZ in *;
   (split; [ exact Hbounds_left | ]);
   cbv [interp_flat_type] in *;
@@ -367,11 +369,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   destruct_head' ZBounds.bounds;
   unfold_is_bounded_in H1;
   simpl @fe5211_32WToZ; simpl @wire_digitsWToZ;
-  unfold_is_bounded;
   destruct_head' and;
   Z.ltb_to_lt;
   change WordW.wordWToZ with word64ToZ in *;
-  repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity.
+  unfold_is_bounded;
+  Z.ltb_to_lt;
+  try omega; try reflexivity.
 
 
 Ltac rexpr_correct :=