1 files changed, 9 insertions, 26 deletions
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
index 916659ab5..62b1ef328 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
@@ -40,37 +40,20 @@ Section BoundedField25p5.
   Let phi : feBW -> F m :=
     fun x => montgomery_to_F (eval x).
 
+  Local Ltac op_sig_side_conditions_t _ :=
+    try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption.
+
   (* TODO : change this to field once field isomorphism happens *)
   Definition sub
     : { sub : feBW_small -> feBW_small -> feBW_small
       | forall A B, phi (sub A B) = F.sub (phi A) (phi B) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ]
-      => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b)
-    end.
-    intros a b.
-    cbv [feBW_of_feBW_small].
-    eexists_sig_etransitivity. all:cbv [phi eval].
-    rewrite <- (proj1 (proj2_sig sub))
-      by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption).
-    reflexivity.
-    apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
-    Associativity.sig_sig_assoc.
-    apply sig_conj_by_impl2.
-    { intros ? H; cbv [eval]; rewrite H; clear H.
-      apply (proj2 (proj2_sig sub)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (subZ := proj1_sig sub).
-    context_to_dlet_in_rhs subZ; cbv [subZ].
-    cbv beta iota delta [sub sub' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
-    reflexivity.
-    sig_dlet_in_rhs_to_context.
-    apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
-    do 2 match goal with
-         | [ H : feBW_small |- _ ] => destruct H as [? _]
-         end.
+    start_preglue.
+    all:cbv [feBW_of_feBW_small eval].
+    do_rewrite_with_sig_by sub op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval sub_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     (*     Set Ltac Profiling.