Copy over better prefreeze

12 files changed, 84 insertions, 42 deletions

diff --git a/src/SpecificGen/GF2213_32Bounded.v b/src/SpecificGen/GF2213_32Bounded.v
index 2947aacfc..e274923d6 100644
--- a/src/SpecificGen/GF2213_32Bounded.v
+++ b/src/SpecificGen/GF2213_32Bounded.v
@@ -150,7 +150,8 @@ Proof.
   { match goal with
     |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
@@ -169,12 +170,13 @@ Proof.
   end. }
 
 
-  unfold_is_bounded.
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *;
+  preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
+  Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
diff --git a/src/SpecificGen/GF2213_32BoundedCommon.v b/src/SpecificGen/GF2213_32BoundedCommon.v
index 8caf225aa..df7031c2c 100644
--- a/src/SpecificGen/GF2213_32BoundedCommon.v
+++ b/src/SpecificGen/GF2213_32BoundedCommon.v
@@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H :=
        unfold_is_bounded_in' H2
   | _ => idtac
   end.
-Ltac unfold_is_bounded_in H :=
+Ltac preunfold_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;
+  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.
+Ltac unfold_is_bounded_in H :=
+  preunfold_is_bounded_in H;
   unfold_is_bounded_in' H.
 
-Ltac unfold_is_bounded :=
+Ltac preunfold_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];
+  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].
+
+Ltac unfold_is_bounded :=
+  preunfold_is_bounded;
   repeat match goal with
          | [ |- andb _ _ = true ] => apply andb_true_intro
          | [ |- and _ _ ] => split
diff --git a/src/SpecificGen/GF2519_32Bounded.v b/src/SpecificGen/GF2519_32Bounded.v
index ca448e458..facfc1a9f 100644
--- a/src/SpecificGen/GF2519_32Bounded.v
+++ b/src/SpecificGen/GF2519_32Bounded.v
@@ -150,7 +150,8 @@ Proof.
   { match goal with
     |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
@@ -169,12 +170,13 @@ Proof.
   end. }
 
 
-  unfold_is_bounded.
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *;
+  preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
+  Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
diff --git a/src/SpecificGen/GF2519_32BoundedCommon.v b/src/SpecificGen/GF2519_32BoundedCommon.v
index 998dd899d..0830e8438 100644
--- a/src/SpecificGen/GF2519_32BoundedCommon.v
+++ b/src/SpecificGen/GF2519_32BoundedCommon.v
@@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H :=
        unfold_is_bounded_in' H2
   | _ => idtac
   end.
-Ltac unfold_is_bounded_in H :=
+Ltac preunfold_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;
+  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.
+Ltac unfold_is_bounded_in H :=
+  preunfold_is_bounded_in H;
   unfold_is_bounded_in' H.
 
-Ltac unfold_is_bounded :=
+Ltac preunfold_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];
+  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].
+
+Ltac unfold_is_bounded :=
+  preunfold_is_bounded;
   repeat match goal with
          | [ |- andb _ _ = true ] => apply andb_true_intro
          | [ |- and _ _ ] => split
diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v
index 7dddfe2c5..748cf05eb 100644
--- a/src/SpecificGen/GF25519_32Bounded.v
+++ b/src/SpecificGen/GF25519_32Bounded.v
@@ -150,7 +150,8 @@ Proof.
   { match goal with
     |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
@@ -169,12 +170,13 @@ Proof.
   end. }
 
 
-  unfold_is_bounded.
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *;
+  preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
+  Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v
index 4c186fd26..1695681c4 100644
--- a/src/SpecificGen/GF25519_32BoundedCommon.v
+++ b/src/SpecificGen/GF25519_32BoundedCommon.v
@@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H :=
        unfold_is_bounded_in' H2
   | _ => idtac
   end.
-Ltac unfold_is_bounded_in H :=
+Ltac preunfold_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;
+  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.
+Ltac unfold_is_bounded_in H :=
+  preunfold_is_bounded_in H;
   unfold_is_bounded_in' H.
 
-Ltac unfold_is_bounded :=
+Ltac preunfold_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];
+  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].
+
+Ltac unfold_is_bounded :=
+  preunfold_is_bounded;
   repeat match goal with
          | [ |- andb _ _ = true ] => apply andb_true_intro
          | [ |- and _ _ ] => split
diff --git a/src/SpecificGen/GF25519_64Bounded.v b/src/SpecificGen/GF25519_64Bounded.v
index 71b859d32..6dedca56b 100644
--- a/src/SpecificGen/GF25519_64Bounded.v
+++ b/src/SpecificGen/GF25519_64Bounded.v
@@ -150,7 +150,8 @@ Proof.
   { match goal with
     |- (_,word128ToZ (_ ^- (Interpretations128.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord128 with Interpretations128.WordW.ZToWordW in *.
+    change ZToWord128 with Interpretations128.WordW.ZToWordW in *.
+    preunfold_is_bounded.
   rewrite !Interpretations128.WordW.wordWToZ_sub;
   rewrite !Interpretations128.WordW.wordWToZ_land;
   rewrite !Interpretations128.WordW.wordWToZ_ZToWordW;
@@ -169,12 +170,13 @@ Proof.
   end. }
 
 
-  unfold_is_bounded.
-  change ZToWord128 with Interpretations128.WordW.ZToWordW in *.
+  change ZToWord128 with Interpretations128.WordW.ZToWordW in *;
+  preunfold_is_bounded.
   rewrite !Interpretations128.WordW.wordWToZ_sub;
   rewrite !Interpretations128.WordW.wordWToZ_land;
   rewrite !Interpretations128.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
+  Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v
index d1e3c6407..3d3a761af 100644
--- a/src/SpecificGen/GF25519_64BoundedCommon.v
+++ b/src/SpecificGen/GF25519_64BoundedCommon.v
@@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H :=
        unfold_is_bounded_in' H2
   | _ => idtac
   end.
-Ltac unfold_is_bounded_in H :=
+Ltac preunfold_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;
+  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.
+Ltac unfold_is_bounded_in H :=
+  preunfold_is_bounded_in H;
   unfold_is_bounded_in' H.
 
-Ltac unfold_is_bounded :=
+Ltac preunfold_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];
+  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].
+
+Ltac unfold_is_bounded :=
+  preunfold_is_bounded;
   repeat match goal with
          | [ |- andb _ _ = true ] => apply andb_true_intro
          | [ |- and _ _ ] => split
diff --git a/src/SpecificGen/GF41417_32Bounded.v b/src/SpecificGen/GF41417_32Bounded.v
index be7cf5714..fdcbe21ea 100644
--- a/src/SpecificGen/GF41417_32Bounded.v
+++ b/src/SpecificGen/GF41417_32Bounded.v
@@ -150,7 +150,8 @@ Proof.
   { match goal with
     |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
@@ -169,12 +170,13 @@ Proof.
   end. }
 
 
-  unfold_is_bounded.
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *;
+  preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
+  Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v
index fec786e23..92a90bd16 100644
--- a/src/SpecificGen/GF41417_32BoundedCommon.v
+++ b/src/SpecificGen/GF41417_32BoundedCommon.v
@@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H :=
        unfold_is_bounded_in' H2
   | _ => idtac
   end.
-Ltac unfold_is_bounded_in H :=
+Ltac preunfold_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;
+  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.
+Ltac unfold_is_bounded_in H :=
+  preunfold_is_bounded_in H;
   unfold_is_bounded_in' H.
 
-Ltac unfold_is_bounded :=
+Ltac preunfold_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];
+  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].
+
+Ltac unfold_is_bounded :=
+  preunfold_is_bounded;
   repeat match goal with
          | [ |- andb _ _ = true ] => apply andb_true_intro
          | [ |- and _ _ ] => split
diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v
index c879a3b19..ca0fdc26c 100644
--- a/src/SpecificGen/GF5211_32Bounded.v
+++ b/src/SpecificGen/GF5211_32Bounded.v
@@ -150,7 +150,8 @@ Proof.
   { match goal with
     |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
@@ -169,12 +170,13 @@ Proof.
   end. }
 
 
-  unfold_is_bounded.
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *;
+  preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
+  Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v
index 911fdb5ba..a12b1287c 100644
--- a/src/SpecificGen/GF5211_32BoundedCommon.v
+++ b/src/SpecificGen/GF5211_32BoundedCommon.v
@@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H :=
        unfold_is_bounded_in' H2
   | _ => idtac
   end.
-Ltac unfold_is_bounded_in H :=
+Ltac preunfold_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;
+  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.
+Ltac unfold_is_bounded_in H :=
+  preunfold_is_bounded_in H;
   unfold_is_bounded_in' H.
 
-Ltac unfold_is_bounded :=
+Ltac preunfold_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];
+  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].
+
+Ltac unfold_is_bounded :=
+  preunfold_is_bounded;
   repeat match goal with
          | [ |- andb _ _ = true ] => apply andb_true_intro
          | [ |- and _ _ ] => split