Factor out some of the preglue synthesis code

This makes it a bit more uniform, and hopefully more automatable and
packageable.  Unfortunately, there's still no spec for this part of the
pipeline, so the tactics simply aggregate common patterns.

Alas, this also makes things a bit slower; I suspect that [Defined] is
the place where things are slower.

After     | File Name                                          | Before    || Change
---------------------------------------------------------------------------------------
13m51.14s | Total                                              | 12m59.29s || +0m51.84s
---------------------------------------------------------------------------------------
1m54.18s  | Specific/IntegrationTestKaratsubaMul               | 1m43.12s  || +0m11.06s
1m38.97s  | Specific/IntegrationTestLadderstep130              | 1m30.26s  || +0m08.70s
2m19.75s  | Specific/NISTP256/AMD64/femul                      | 2m14.08s  || +0m05.66s
0m39.90s  | Specific/IntegrationTestMontgomeryP256_128         | 0m34.21s  || +0m05.68s
0m21.95s  | Specific/NISTP256/AMD64/fesub                      | 0m19.23s  || +0m02.71s
0m21.37s  | Specific/NISTP256/AMD64/feadd                      | 0m18.82s  || +0m02.55s
0m21.02s  | Specific/X25519/C64/femul                          | 0m18.32s  || +0m02.69s
0m20.53s  | Specific/IntegrationTestFreeze                     | 0m23.26s  || -0m02.73s
0m18.28s  | Specific/IntegrationTestMontgomeryP256_128_Sub     | 0m15.32s  || +0m02.96s
0m18.20s  | Specific/IntegrationTestMontgomeryP256_128_Add     | 0m15.52s  || +0m02.67s
0m16.35s  | Specific/IntegrationTestMontgomeryP256_128_Opp     | 0m13.52s  || +0m02.83s
0m13.92s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s  || +0m02.08s
0m18.23s  | Specific/NISTP256/AMD64/MontgomeryP256             | 0m16.62s  || +0m01.60s
0m15.54s  | Specific/IntegrationTestSub                        | 0m14.53s  || +0m01.00s
0m14.78s  | Specific/X25519/C64/fesquare                       | 0m13.13s  || +0m01.64s
0m13.71s  | Specific/NISTP256/AMD64/fenz                       | 0m12.69s  || +0m01.02s
3m14.34s  | Specific/X25519/C64/ladderstep                     | 3m14.32s  || +0m00.02s
0m16.54s  | Specific/NISTP256/AMD64/feopp                      | 0m16.48s  || +0m00.05s
0m12.21s  | Specific/MontgomeryP256_128                        | 0m12.70s  || -0m00.48s
0m00.73s  | Specific/IntegrationTestTemporaryMiscCommon        | 0m00.72s  || +0m00.01s
0m00.64s  | Specific/IntegrationTestDisplayCommon              | 0m00.60s  || +0m00.04s

19 files changed, 554 insertions, 417 deletions

diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index 62ff363e2..18cee5114 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -42,33 +42,28 @@ Section BoundedField25p5.
   Let phi : feBW -> F m :=
     fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
+  Lemma feBW_bounded (a : feBW)
+    : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
+  Proof.
+    destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
+    revert H.
+    cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
+    repeat match goal with
+           | [ |- context[wt ?n] ]
+             => let v := (eval compute in (wt n)) in change (wt n) with v
+           end.
+    intro; destruct_head'_and.
+    omega.
+  Qed.
+
   (* TODO : change this to field once field isomorphism happens *)
   Definition freeze :
     { freeze : feBW -> feBW
     | forall a, phi (freeze a) = phi a }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, ?phi (f a) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => phi f = rhs a)
-    end.
-    intros a.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- (proj2_sig freeze_sig).
-    { set (freezeZ := proj1_sig freeze_sig).
-      context_to_dlet_in_rhs freezeZ.
-      cbv beta iota delta [freezeZ proj1_sig freeze_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
-      reflexivity. }
-    { destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
-      revert H.
-      cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
-      repeat match goal with
-             | [ |- context[wt ?n] ]
-               => let v := (eval compute in (wt n)) in change (wt n) with v
-             end.
-      intro; destruct_head'_and.
-      omega. }
-    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)).
+    start_preglue.
+    do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime.
+    all:fin_preglue.
     (* jgross start here! *)
     (*Set Ltac Profiling.*)
     Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v
index 9dc49ca00..0a29973a1 100644
--- a/src/Specific/IntegrationTestKaratsubaMul.v
+++ b/src/Specific/IntegrationTestKaratsubaMul.v
@@ -46,21 +46,9 @@ Section BoundedField25p5.
     { mul : feBW -> feBW -> feBW
     | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
-      => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
-    end.
-    intros a b.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- (proj2_sig mul_sig).
-    symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
-    set (carry_mulZ := fun a b => proj1_sig carry_sig (proj1_sig mul_sig a b)).
-    change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?b)) with (carry_mulZ a b).
-    context_to_dlet_in_rhs carry_mulZ.
-    cbv beta iota delta [carry_mulZ proj1_sig mul_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
-    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)).
+    start_preglue.
+    do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
+    all:fin_preglue.
     (* jgross start here! *)
     (*Set Ltac Profiling.*)
     Time refine_reflectively.
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v
index 541dcaee8..4dd01d018 100644
--- a/src/Specific/IntegrationTestLadderstep130.v
+++ b/src/Specific/IntegrationTestLadderstep130.v
@@ -77,12 +77,7 @@ Section BoundedField25p5.
             /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
            /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
   Proof.
-    lazymatch goal with
-    | [ |- { op | forall (a:?A) (b:?B) (c:?C),
-               let v := op a b c in
-               @?P a b c v } ]
-      => refine (@lift3_sig A B C _ P _)
-    end.
+    apply_lift_sig.
     intros a b c; cbv beta iota zeta.
     lazymatch goal with
     | [ |- { e | ?A -> ?B -> ?C -> @?E e } ]
@@ -102,11 +97,12 @@ Section BoundedField25p5.
       cbv [proj1_sig]; cbv [Mxzladderstep_sig].
       context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _).
       cbv [M.xzladderstep a24_sig].
-      do 4 lazymatch goal with
-           | [ |- context[@proj1_sig ?a ?b ?f_sig _] ]
-             => context_to_dlet_in_rhs (@proj1_sig a b f_sig)
-           end.
-      cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd].
+      repeat lazymatch goal with
+             | [ |- context[@proj1_sig ?a ?b ?f_sig _] ]
+               => context_to_dlet_in_rhs (@proj1_sig a b f_sig)
+             end.
+      cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig].
+      cbv_runtime.
       refine (proj2 FINAL). }
     subst feW feW_bounded; cbv beta.
     (* jgross start here! *)
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128.v b/src/Specific/IntegrationTestMontgomeryP256_128.v
index 00f751908..feca5ad9a 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128.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 mul
     : { mul : feBW_small -> feBW_small -> feBW_small
       | forall A B, phi (mul A B) = F.mul (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 mulmod_256))
-      by (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 mulmod_256)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (mulmodZ := proj1_sig mulmod_256).
-    context_to_dlet_in_rhs mulmodZ; cbv [mulmodZ].
-    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' 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 mulmod_256 op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval mulmod_256_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     (*     Set Ltac Profiling.
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v
index 367f63a0b..a9fea3ef1 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Add.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 add
     : { add : feBW_small -> feBW_small -> feBW_small
       | forall A B, phi (add A B) = F.add (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 add))
-      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 add)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (addZ := proj1_sig add).
-    context_to_dlet_in_rhs addZ; cbv [addZ].
-    cbv beta iota delta [add add' 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 add op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval add_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     (*     Set Ltac Profiling.
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
index 6adeac3f9..3c605e348 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
@@ -44,18 +44,16 @@ 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 nonzero
     : { nonzero : feBW_small -> BoundedWord  1 bitwidth bound1
       | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a)
-    end.
-    intros a.
-    cbv [feBW_of_feBW_small].
-    eexists_sig_etransitivity. all:cbv [phi eval].
+    apply_lift_sig; intros; eexists_sig_etransitivity.
+    all:cbv [feBW_of_feBW_small phi eval].
     refine (_ : (if Decidable.dec (_ = 0) then true else false) = _).
     lazymatch goal with
     | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ]
@@ -65,7 +63,7 @@ Section BoundedField25p5.
            | ]
     end.
     etransitivity; [ | eapply (proj2_sig nonzero) ];
-      [ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ].
+      [ | solve [ op_sig_side_conditions_t () ].. ].
     reflexivity.
     let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in
     apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _).
@@ -78,9 +76,8 @@ Section BoundedField25p5.
           try reflexivity.
         Z.ltb_to_lt; congruence. } }
     eexists_sig_etransitivity.
-    set (nonzeroZ := proj1_sig nonzero).
-    context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
-    cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    do_set_sig nonzero.
+    cbv_runtime.
     reflexivity.
     sig_dlet_in_rhs_to_context.
     match goal with
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
index 1a609d7b4..1869a7952 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.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 opp
     : { opp : feBW_small -> feBW_small
       | forall A, phi (opp A) = F.opp (phi A) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, ?phi (?proj (f a)) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => phi (proj f) = rhs a)
-    end.
-    intros a.
-    cbv [feBW_of_feBW_small].
-    eexists_sig_etransitivity. all:cbv [phi eval].
-    rewrite <- (proj1 (proj2_sig opp))
-      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 opp)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (oppZ := proj1_sig opp).
-    context_to_dlet_in_rhs oppZ; cbv [oppZ].
-    cbv beta iota delta [opp opp' proj1_sig MontgomeryAPI.T lift1_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)).
-    match goal with
-    | [ H : feBW_small |- _ ] => destruct H as [? _]
-    end.
+    start_preglue.
+    all:cbv [feBW_of_feBW_small eval].
+    do_rewrite_with_sig_by opp op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval opp_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     (*     Set Ltac Profiling.
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.
diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v
index 4e012486c..2e46d22eb 100644
--- a/src/Specific/IntegrationTestTemporaryMiscCommon.v
+++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v
@@ -1,6 +1,12 @@
 (*** XXX TODO MOVE ALL THINGS IN THIS FILE TO BETTER PLACES *)
+Require Import Coq.ZArith.BinInt.
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Sigma.Lift.
+Require Import Crypto.Util.Sigma.Associativity.
+Require Import Crypto.Util.Sigma.MapProjections.
+Require Import Crypto.Util.Tactics.MoveLetIn.
+Require Import Crypto.Util.Tactics.DestructHead.
 
 Definition adjust_tuple2_tuple2_sig {A P Q}
            (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) }
@@ -78,3 +84,113 @@ Definition sig_conj_by_impl2 {A} {P Q : A -> Prop} (H : forall a : A, Q a -> P a
            (H' : { a : A | Q a })
   : { a : A | P a /\ Q a }
   := let (a, p) := H' in exist _ a (conj (H a p) p).
+
+
+(** [apply_lift_sig] picks out which version of the [liftN_sig] lemma
+    to apply, and builds the appropriate arguments *)
+Ltac make_P_for_apply_lift_sig P :=
+  lazymatch P with
+  | fun (f : ?F) => forall (a : ?A), @?P f a
+    => constr:(fun (a : A)
+               => ltac:(lazymatch constr:(fun (f : F)
+                                          => ltac:(let v := (eval cbv beta in (P f a)) in
+                                                   lazymatch (eval pattern (f a) in v) with
+                                                   | ?k _ => exact k
+                                                   end))
+                        with
+                        | fun _ => ?P
+                          => let v := make_P_for_apply_lift_sig P in
+                             exact v
+                        end))
+  | _ => P
+  end.
+Ltac apply_lift_sig :=
+  let P := lazymatch goal with |- sig ?P => P end in
+  let P := make_P_for_apply_lift_sig P in
+  lazymatch goal with
+  | [ |- { f | forall a b c d e, _ } ]
+    => fail "apply_lift_sig does not yet support ≥ 5 binders"
+  | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C) (d : ?D), _ } ]
+    => apply (@lift4_sig A B C D _ P)
+  | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C), _ } ]
+    => apply (@lift3_sig A B C _ P)
+  | [ |- { f | forall (a : ?A) (b : ?B), _ } ]
+    => apply (@lift2_sig A B _ P)
+  | [ |- { f | forall (a : ?A), _ } ]
+    => apply (@lift1_sig A _ P)
+  | [ |- { f | _ } ]
+    => idtac
+  end.
+Ltac start_preglue :=
+  apply_lift_sig; intros;
+  let phi := lazymatch goal with |- { f | ?phi _ = _ } => phi end in
+  eexists_sig_etransitivity; cbv [phi].
+Ltac do_set_sig f_sig :=
+  let fZ := fresh f_sig in
+  set (fZ := proj1_sig f_sig);
+  context_to_dlet_in_rhs fZ; cbv beta delta [fZ];
+  try cbv beta iota delta [proj1_sig f_sig];
+  cbv beta iota delta [fst snd].
+Ltac do_rewrite_with_sig_by f_sig by_tac :=
+  let lem := constr:(proj2_sig f_sig) in
+  let lemT := type of lem in
+  let lemT := (eval cbv beta zeta in lemT) in
+  rewrite <- (lem : lemT) by by_tac ();
+  do_set_sig f_sig.
+Ltac do_rewrite_with_sig f_sig := do_rewrite_with_sig_by f_sig ltac:(fun _ => idtac).
+Ltac do_rewrite_with_1sig_add_carry_by f_sig carry_sig by_tac :=
+  let fZ := fresh f_sig in
+  rewrite <- (proj2_sig f_sig) by by_tac ();
+  symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry;
+  pose (fun a => proj1_sig carry_sig (proj1_sig f_sig a)) as fZ;
+  lazymatch goal with
+  | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a)] ]
+    => let G' := context G[fZ a] in change G'
+  end;
+  context_to_dlet_in_rhs fZ; cbv beta delta [fZ];
+  try cbv beta iota delta [proj1_sig f_sig carry_sig];
+  cbv beta iota delta [fst snd].
+Ltac do_rewrite_with_1sig_add_carry f_sig carry_sig := do_rewrite_with_1sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac).
+Ltac do_rewrite_with_2sig_add_carry_by f_sig carry_sig by_tac :=
+  let fZ := fresh f_sig in
+  rewrite <- (proj2_sig f_sig) by by_tac ();
+  symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry;
+  pose (fun a b => proj1_sig carry_sig (proj1_sig f_sig a b)) as fZ;
+  lazymatch goal with
+  | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a ?b)] ]
+    => let G' := context G[fZ a b] in change G'
+  end;
+  context_to_dlet_in_rhs fZ; cbv beta delta [fZ];
+  try cbv beta iota delta [proj1_sig f_sig carry_sig];
+  cbv beta iota delta [fst snd].
+Ltac do_rewrite_with_2sig_add_carry f_sig carry_sig := do_rewrite_with_2sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac).
+Ltac fin_preglue :=
+  [ > reflexivity
+  | repeat 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)) ].
+
+Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t :=
+  let feBW_small := lazymatch goal with |- { f : ?feBW_small | _ } => feBW_small end in
+  Associativity.sig_sig_assoc;
+  apply sig_conj_by_impl2;
+  [ let H := fresh in
+    intros ? H;
+    try lazymatch goal with
+        | [ |- (?eval _ < _)%Z ]
+          => cbv [eval]
+        end;
+    rewrite H; clear H;
+    eapply Z.le_lt_trans;
+      [ apply Z.eq_le_incl, f_equal | apply op_bounded ];
+      [ repeat match goal with
+               | [ |- ?f ?x = ?g ?y ]
+                 => is_evar y; unify x y;
+                    apply (f_equal (fun fg => fg x))
+               end;
+        clear; abstract reflexivity
+      | .. ];
+      op_sig_side_conditions_t ()
+  | 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));
+    repeat match goal with
+           | [ H : feBW_small |- _ ] => destruct H as [? _]
+           end ].
diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v
index 9c0336503..b3df2a409 100644
--- a/src/Specific/MontgomeryP256_128.v
+++ b/src/Specific/MontgomeryP256_128.v
@@ -201,15 +201,16 @@ Proof.*)
 Definition montgomery_to_F (v : Z) : F m
   := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
 
-Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | let eval := MontgomeryAPI.eval (Z.pos r) in
-                          (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                              montgomery_to_F (eval (f A B))
-                              = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
-                          /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                                     (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                                 (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
+Definition mulmod_256_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+              (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+          montgomery_to_F (eval (f A B))
+          = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
+      /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                 (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+             (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
 Proof.
   exists (proj1_sig mulmod_256'').
   abstract (
@@ -226,6 +227,26 @@ Proof.
     ).
 Defined.
 
+Definition mulmod_256
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        montgomery_to_F (eval (f A B))
+        = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }.
+Proof.
+  let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in
+  (exists v).
+  abstract apply (proj2_sig mulmod_256_ext).
+Defined.
+
+Lemma mulmod_256_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+           (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+      (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z.
+Proof. apply (proj2_sig mulmod_256_ext). Qed.
+
 Local Ltac t_fin :=
   [ > reflexivity
   | repeat match goal with
@@ -241,19 +262,20 @@ Local Ltac t_fin :=
            | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small
            end.. ].
 
-Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> montgomery_to_F (eval (f A B))
-                            = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                           (eval A < eval p256
-                            -> eval B < eval p256
-                            -> 0 <= eval (f A B) < eval p256)))%Z }.
+Definition add_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+           (eval A < eval p256
+            -> eval B < eval p256
+            -> montgomery_to_F (eval (f A B))
+               = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+              (eval A < eval p256
+               -> eval B < eval p256
+               -> 0 <= eval (f A B) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig add').
   abstract (
@@ -266,19 +288,20 @@ Proof.
     ).
 Defined.
 
-Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> montgomery_to_F (eval (f A B))
-                            = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> 0 <= eval (f A B) < eval p256)))%Z }.
+Definition sub_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+           (eval A < eval p256
+            -> eval B < eval p256
+            -> montgomery_to_F (eval (f A B))
+               = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+              (eval A < eval p256
+               -> eval B < eval p256
+               -> 0 <= eval (f A B) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig sub').
   abstract (
@@ -291,15 +314,16 @@ Proof.
     ).
 Defined.
 
-Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                        (eval A < eval p256
-                         -> montgomery_to_F (eval (f A))
-                            = (F.opp (montgomery_to_F (eval A)))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                           (eval A < eval p256
-                            -> 0 <= eval (f A) < eval p256)))%Z }.
+Definition opp_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+           (eval A < eval p256
+            -> montgomery_to_F (eval (f A))
+               = (F.opp (montgomery_to_F (eval A)))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+              (eval A < eval p256
+               -> 0 <= eval (f A) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig opp').
   abstract (
@@ -312,11 +336,12 @@ Proof.
     ).
 Defined.
 
-Definition nonzero : { f:Tuple.tuple Z sz -> Z
-                     | let eval := MontgomeryAPI.eval (Z.pos r) in
-                       forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                         (eval A < eval p256
-                          -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Definition nonzero_ext
+  : { f:Tuple.tuple Z sz -> Z
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
 Proof.
   exists (proj1_sig nonzero').
   abstract (
@@ -334,5 +359,86 @@ Proof.
     ).
 Defined.
 
+Definition add
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> montgomery_to_F (eval (f A B))
+            = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in
+  (exists v).
+  abstract apply (proj2_sig add_ext).
+Defined.
+
+Lemma add_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> 0 <= eval (proj1_sig add A B) < eval p256))%Z.
+Proof. apply (proj2_sig add_ext). Qed.
+
+Definition sub
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> montgomery_to_F (eval (f A B))
+            = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in
+  (exists v).
+  abstract apply (proj2_sig sub_ext).
+Defined.
+
+Lemma sub_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z.
+Proof. apply (proj2_sig sub_ext). Qed.
+
+Definition opp
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> montgomery_to_F (eval (f A))
+            = (F.opp (montgomery_to_F (eval A)))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in
+  (exists v).
+  abstract apply (proj2_sig opp_ext).
+Defined.
+
+Lemma opp_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> 0 <= eval (proj1_sig opp A) < eval p256))%Z.
+Proof. apply (proj2_sig opp_ext). Qed.
+
+Definition nonzero
+  : { f:Tuple.tuple Z sz -> Z
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in
+  (exists v).
+  abstract apply (proj2_sig nonzero_ext).
+Defined.
+
+
 Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero).
 Print Assumptions for_assumptions.
diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
index e709cc3ea..e8b25a781 100644
--- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v
+++ b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
@@ -195,15 +195,17 @@ Proof.*)
 Definition montgomery_to_F (v : Z) : F m
   := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
 
-Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | let eval := MontgomeryAPI.eval (Z.pos r) in
-                          (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                              montgomery_to_F (eval (f A B))
-                              = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
-                          /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                                     (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                                 (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
+
+Definition mulmod_256_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+              (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+          montgomery_to_F (eval (f A B))
+          = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
+      /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                 (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+             (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
 Proof.
   exists (proj1_sig mulmod_256'').
   abstract (
@@ -220,6 +222,26 @@ Proof.
     ).
 Defined.
 
+Definition mulmod_256
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        montgomery_to_F (eval (f A B))
+        = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }.
+Proof.
+  let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in
+  (exists v).
+  abstract apply (proj2_sig mulmod_256_ext).
+Defined.
+
+Lemma mulmod_256_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+           (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+      (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z.
+Proof. apply (proj2_sig mulmod_256_ext). Qed.
+
 Local Ltac t_fin :=
   [ > reflexivity
   | repeat match goal with
@@ -235,19 +257,20 @@ Local Ltac t_fin :=
            | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small
            end.. ].
 
-Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> montgomery_to_F (eval (f A B))
-                            = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                           (eval A < eval p256
-                            -> eval B < eval p256
-                            -> 0 <= eval (f A B) < eval p256)))%Z }.
+Definition add_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+           (eval A < eval p256
+            -> eval B < eval p256
+            -> montgomery_to_F (eval (f A B))
+               = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+              (eval A < eval p256
+               -> eval B < eval p256
+               -> 0 <= eval (f A B) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig add').
   abstract (
@@ -260,19 +283,20 @@ Proof.
     ).
 Defined.
 
-Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> montgomery_to_F (eval (f A B))
-                            = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> 0 <= eval (f A B) < eval p256)))%Z }.
+Definition sub_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+           (eval A < eval p256
+            -> eval B < eval p256
+            -> montgomery_to_F (eval (f A B))
+               = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+              (eval A < eval p256
+               -> eval B < eval p256
+               -> 0 <= eval (f A B) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig sub').
   abstract (
@@ -285,15 +309,16 @@ Proof.
     ).
 Defined.
 
-Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                        (eval A < eval p256
-                         -> montgomery_to_F (eval (f A))
-                            = (F.opp (montgomery_to_F (eval A)))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                           (eval A < eval p256
-                            -> 0 <= eval (f A) < eval p256)))%Z }.
+Definition opp_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+           (eval A < eval p256
+            -> montgomery_to_F (eval (f A))
+               = (F.opp (montgomery_to_F (eval A)))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+              (eval A < eval p256
+               -> 0 <= eval (f A) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig opp').
   abstract (
@@ -306,11 +331,12 @@ Proof.
     ).
 Defined.
 
-Definition nonzero : { f:Tuple.tuple Z sz -> Z
-                     | let eval := MontgomeryAPI.eval (Z.pos r) in
-                       forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                         (eval A < eval p256
-                          -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Definition nonzero_ext
+  : { f:Tuple.tuple Z sz -> Z
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
 Proof.
   exists (proj1_sig nonzero').
   abstract (
@@ -328,5 +354,85 @@ Proof.
     ).
 Defined.
 
+Definition add
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> montgomery_to_F (eval (f A B))
+            = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in
+  (exists v).
+  abstract apply (proj2_sig add_ext).
+Defined.
+
+Lemma add_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> 0 <= eval (proj1_sig add A B) < eval p256))%Z.
+Proof. apply (proj2_sig add_ext). Qed.
+
+Definition sub
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> montgomery_to_F (eval (f A B))
+            = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in
+  (exists v).
+  abstract apply (proj2_sig sub_ext).
+Defined.
+
+Lemma sub_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z.
+Proof. apply (proj2_sig sub_ext). Qed.
+
+Definition opp
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> montgomery_to_F (eval (f A))
+            = (F.opp (montgomery_to_F (eval A)))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in
+  (exists v).
+  abstract apply (proj2_sig opp_ext).
+Defined.
+
+Lemma opp_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> 0 <= eval (proj1_sig opp A) < eval p256))%Z.
+Proof. apply (proj2_sig opp_ext). Qed.
+
+Definition nonzero
+  : { f:Tuple.tuple Z sz -> Z
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in
+  (exists v).
+  abstract apply (proj2_sig nonzero_ext).
+Defined.
+
 Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero).
 Print Assumptions for_assumptions.
diff --git a/src/Specific/NISTP256/AMD64/feadd.v b/src/Specific/NISTP256/AMD64/feadd.v
index 1ea0fbc35..5de6fc03a 100644
--- a/src/Specific/NISTP256/AMD64/feadd.v
+++ b/src/Specific/NISTP256/AMD64/feadd.v
@@ -39,37 +39,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 add
     : { add : feBW_small -> feBW_small -> feBW_small
       | forall A B, phi (add A B) = F.add (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 add))
-      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 add)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (addZ := proj1_sig add).
-    context_to_dlet_in_rhs addZ; cbv [addZ].
-    cbv beta iota delta [add add' 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 add op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval add_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     (*     Set Ltac Profiling.
diff --git a/src/Specific/NISTP256/AMD64/femul.v b/src/Specific/NISTP256/AMD64/femul.v
index d600869bd..f87e6d26b 100644
--- a/src/Specific/NISTP256/AMD64/femul.v
+++ b/src/Specific/NISTP256/AMD64/femul.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 mul
     : { mul : feBW_small -> feBW_small -> feBW_small
       | forall A B, phi (mul A B) = F.mul (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 mulmod_256))
-      by (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 mulmod_256)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (mulmodZ := proj1_sig mulmod_256).
-    context_to_dlet_in_rhs mulmodZ; cbv [mulmodZ].
-    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
-    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 mulmod_256 op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval mulmod_256_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v
index cfea6e957..b46460550 100644
--- a/src/Specific/NISTP256/AMD64/fenz.v
+++ b/src/Specific/NISTP256/AMD64/fenz.v
@@ -44,18 +44,16 @@ 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 nonzero
     : { nonzero : feBW_small -> BoundedWord  1 bitwidth bound1
       | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a)
-    end.
-    intros a.
-    cbv [feBW_of_feBW_small].
-    eexists_sig_etransitivity. all:cbv [phi eval].
+    apply_lift_sig; intros; eexists_sig_etransitivity.
+    all:cbv [feBW_of_feBW_small phi eval].
     refine (_ : (if Decidable.dec (_ = 0) then true else false) = _).
     lazymatch goal with
     | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ]
@@ -65,7 +63,7 @@ Section BoundedField25p5.
            | ]
     end.
     etransitivity; [ | eapply (proj2_sig nonzero) ];
-      [ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ].
+      [ | solve [ op_sig_side_conditions_t () ].. ].
     reflexivity.
     let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in
     apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _).
@@ -78,9 +76,8 @@ Section BoundedField25p5.
           try reflexivity.
         Z.ltb_to_lt; congruence. } }
     eexists_sig_etransitivity.
-    set (nonzeroZ := proj1_sig nonzero).
-    context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
-    cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    do_set_sig nonzero.
+    cbv_runtime.
     reflexivity.
     sig_dlet_in_rhs_to_context.
     match goal with
diff --git a/src/Specific/NISTP256/AMD64/feopp.v b/src/Specific/NISTP256/AMD64/feopp.v
index ef4ea6aa6..14342c238 100644
--- a/src/Specific/NISTP256/AMD64/feopp.v
+++ b/src/Specific/NISTP256/AMD64/feopp.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 opp
     : { opp : feBW_small -> feBW_small
       | forall A, phi (opp A) = F.opp (phi A) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, ?phi (?proj (f a)) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => phi (proj f) = rhs a)
-    end.
-    intros a.
-    cbv [feBW_of_feBW_small].
-    eexists_sig_etransitivity. all:cbv [phi eval].
-    rewrite <- (proj1 (proj2_sig opp))
-      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 opp)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (oppZ := proj1_sig opp).
-    context_to_dlet_in_rhs oppZ; cbv [oppZ].
-    cbv beta iota delta [opp opp' proj1_sig MontgomeryAPI.T lift1_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)).
-    match goal with
-    | [ H : feBW_small |- _ ] => destruct H as [? _]
-    end.
+    start_preglue.
+    all:cbv [feBW_of_feBW_small eval].
+    do_rewrite_with_sig_by opp op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval opp_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     (*     Set Ltac Profiling.
diff --git a/src/Specific/NISTP256/AMD64/fesub.v b/src/Specific/NISTP256/AMD64/fesub.v
index d01471804..adf278faa 100644
--- a/src/Specific/NISTP256/AMD64/fesub.v
+++ b/src/Specific/NISTP256/AMD64/fesub.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.
diff --git a/src/Specific/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v
index 01d629bfb..155bcf9e1 100644
--- a/src/Specific/X25519/C64/femul.v
+++ b/src/Specific/X25519/C64/femul.v
@@ -46,21 +46,9 @@ Section BoundedField25p5.
     { mul : feBW -> feBW -> feBW
     | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
-      => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
-    end.
-    intros a b.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- (proj2_sig mul_sig).
-    symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
-    set (carry_mulZ := fun a b => proj1_sig carry_sig (proj1_sig mul_sig a b)).
-    change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?b)) with (carry_mulZ a b).
-    context_to_dlet_in_rhs carry_mulZ.
-    cbv beta iota delta [carry_mulZ proj1_sig mul_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
-    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)).
+    start_preglue.
+    do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
+    all:fin_preglue.
     (* jgross start here! *)
     (*Set Ltac Profiling.*)
     Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v
index d7d717c61..0bba90c68 100644
--- a/src/Specific/X25519/C64/fesquare.v
+++ b/src/Specific/X25519/C64/fesquare.v
@@ -46,21 +46,9 @@ Section BoundedField25p5.
     { square : feBW -> feBW
     | forall a, phi (square a) = F.mul (phi a) (phi a) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, ?phi (f a) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => phi f = rhs a)
-    end.
-    intros a.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- (proj2_sig square_sig).
-    symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
-    set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a)).
-    change (proj1_sig carry_sig (proj1_sig square_sig ?a)) with (carry_squareZ a).
-    context_to_dlet_in_rhs carry_squareZ.
-    cbv beta iota delta [carry_squareZ proj1_sig square_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
-    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)).
+    start_preglue.
+    do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
+    all:fin_preglue.
     (* jgross start here! *)
     (*Set Ltac Profiling.*)
     Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index b88370a48..ad0037245 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -112,12 +112,7 @@ Section BoundedField25p5.
             /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
            /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
   Proof.
-    lazymatch goal with
-    | [ |- { op | forall (a:?A) (b:?B) (c:?C),
-               let v := op a b c in
-               @?P a b c v } ]
-      => refine (@lift3_sig A B C _ P _)
-    end.
+    apply_lift_sig.
     intros a b c; cbv beta iota zeta.
     lazymatch goal with
     | [ |- { e | ?A -> ?B -> ?C -> @?E e } ]
@@ -137,11 +132,12 @@ Section BoundedField25p5.
       cbv [proj1_sig]; cbv [Mxzladderstep_sig].
       context_to_dlet_in_rhs (@Mxzladderstep _).
       cbv [Mxzladderstep M.xzladderstep a24_sig].
-      do 5 lazymatch goal with
-           | [ |- context[@proj1_sig ?a ?b ?f_sig _] ]
-             => context_to_dlet_in_rhs (@proj1_sig a b f_sig)
-           end.
-      cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig square_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd].
+      repeat lazymatch goal with
+             | [ |- context[@proj1_sig ?a ?b ?f_sig _] ]
+               => context_to_dlet_in_rhs (@proj1_sig a b f_sig)
+             end.
+      cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig square_sig].
+      cbv_runtime.
       refine (proj2 FINAL). }
     subst feW feW_bounded; cbv beta.
     (* jgross start here! *)