Remove slow "intros [a b]"

Hopefully this will help speed up some primes, like:

```
 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─synthesize_with_carry -----------------   0.0% 100.0%       1 4158.848s
└Pipeline.refine_reflectively_gen ------   0.0%  99.0%       1 4117.688s
└ReflectiveTactics.do_reflective_pipelin   0.0%  98.7%       1 4106.804s
└ReflectiveTactics.solve_side_conditions   0.0%  98.7%       1 4106.580s
 ├─UnifyAbstractReflexivity.unify_transf  73.7%  74.5%       8 2283.572s
 ├─ReflectiveTactics.handle_boundedness_   0.0%  18.8%       1  781.616s
 │└intros [a b] ------------------------  18.4%  18.4%      29   33.640s
 └─ReflectiveTactics.do_reify ----------   0.0%   5.4%       1  225.672s
  └Reify.do_reify_abs_goal -------------   4.7%   4.7%       2  196.164s
  └Reify.do_reifyf_goal ----------------   4.7%   4.7%     270  102.004s

src/Specific/solinas32_2e512m569/fesquare (real: 5415.91, user: 5115.86, sys: 27.59, mem: 33162744 ko)
```

and

```
 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─Pipeline.refine_reflectively_gen ------   0.0%  97.8%       1  437.088s
 ├─ReflectiveTactics.do_reflective_pipel   0.0%  94.0%       1  420.396s
 │└ReflectiveTactics.solve_side_conditio   0.0%  94.0%       1  420.232s
 │ ├─ReflectiveTactics.handle_boundednes   0.0%  63.3%       1  283.096s
 │ │└intros [a b] ----------------------  61.9%  61.9%      39   10.288s
 │ ├─ReflectiveTactics.do_reify --------   0.1%  15.8%       1   70.528s
 │ │ ├─Reify.do_reify_abs_goal ---------  12.6%  12.7%       2   56.572s
 │ │ │└Reify.do_reifyf_goal ------------  12.5%  12.5%     180   30.120s
 │ │ │└eexact --------------------------   3.9%   3.9%     180    0.132s
 │ │ └─Reify.Reify_rhs_gen -------------   0.2%   2.9%       1   12.836s
 │ └─UnifyAbstractReflexivity.unify_tran  12.6%  14.5%       8   23.836s
 └─Glue.refine_to_reflective_glue' -----   0.0%   3.7%       1   16.692s
  └Glue.zrange_to_reflective -----------   0.0%   3.7%       1   16.372s
  └Glue.zrange_to_reflective_goal ------   0.4%   2.9%       1   13.084s
  └pose proof  (pf   :   Interpretation.   2.5%   2.5%       1   11.144s
─synthesize ----------------------------   0.0%   2.2%       1    9.988s
└IntegrationTestTemporaryMiscCommon.do_r   0.0%   2.2%       1    9.904s
└change G' -----------------------------   2.2%   2.2%       1    9.812s

src/Specific/solinas32_2e521m1/femul (real: 1165.84, user: 878.68, sys: 9.32, mem: 11218492 ko)
```
and
```
 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─Pipeline.refine_reflectively_gen ------   0.0%  97.6%       1  118.496s
 ├─ReflectiveTactics.do_reflective_pipel   0.0%  93.7%       1  113.844s
 │└ReflectiveTactics.solve_side_conditio   0.0%  93.7%       1  113.772s
 │ ├─ReflectiveTactics.handle_boundednes   0.0%  52.8%       1   64.160s
 │ │└intros [a b] ----------------------  50.9%  50.9%      29    2.420s
 │ ├─ReflectiveTactics.do_reify --------   0.2%  23.7%       1   28.840s
 │ │ ├─Reify.do_reify_abs_goal ---------  17.8%  17.9%       2   21.792s
 │ │ │└Reify.do_reifyf_goal ------------  17.6%  17.7%     135   10.952s
 │ │ │└eexact --------------------------   5.4%   5.4%     135    0.064s
 │ │ └─Reify.Reify_rhs_gen -------------   0.4%   5.3%       1    6.452s
 │ └─UnifyAbstractReflexivity.unify_tran  14.0%  16.4%       8    8.544s
 │  └unify (constr) (constr) -----------   2.0%   2.0%       6    1.460s
 └─Glue.refine_to_reflective_glue' -----   0.0%   3.8%       1    4.644s
  └Glue.zrange_to_reflective -----------   0.0%   3.7%       1    4.472s
  └Glue.zrange_to_reflective_goal ------   0.6%   2.8%       1    3.392s
  └pose proof  (pf   :   Interpretation.   2.1%   2.1%       1    2.564s
─synthesize_with_carry -----------------   0.0%   2.4%       1    2.968s
└IntegrationTestTemporaryMiscCommon.do_r   0.0%   2.4%       1    2.920s
└change G' -----------------------------   2.4%   2.4%       1    2.868s

src/Specific/solinas32_2e255m765/femul (real: 307.37, user: 255.97, sys: 0.81, mem: 4050732 ko)
```
```

A bit of testing suggests that it is, indeed, much better:
```
 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─Pipeline.refine_reflectively_gen ------   0.0%  95.5%       1   60.100s
 ├─ReflectiveTactics.do_reflective_pipel   0.0%  88.7%       1   55.764s
 │└ReflectiveTactics.solve_side_conditio   0.0%  88.3%       1   55.556s
 │ ├─ReflectiveTactics.do_reify --------   0.0%  48.3%       1   30.412s
 │ │└Reify.Reify_rhs_gen ---------------   1.2%  47.8%       1   30.048s
 │ │ ├─Reify.do_reify_abs_goal ---------  36.0%  36.3%       2   22.804s
 │ │ │└Reify.do_reifyf_goal ------------  35.4%  35.6%     117   11.708s
 │ │ │└eexact --------------------------  10.9%  10.9%     117    0.080s
 │ │ ├─rewrite H -----------------------   2.9%   2.9%       1    1.820s
 │ │ └─prove_interp_compile_correct ----   0.0%   2.7%       1    1.724s
 │ │  └rewrite ?EtaInterp.InterpExprEta    2.5%   2.5%       1    1.584s
 │ └─ReflectiveTactics.solve_post_reifie   0.1%  40.0%       1   25.144s
 │  └UnifyAbstractReflexivity.unify_tran  32.0%  37.4%       8   10.584s
 │  └unify (constr) (constr) -----------   4.5%   4.5%       6    1.504s
 └─Glue.refine_to_reflective_glue' -----   0.0%   6.9%       1    4.336s
  └Glue.zrange_to_reflective -----------   0.0%   6.4%       1    4.056s
  └Glue.zrange_to_reflective_goal ------   1.3%   4.9%       1    3.104s
  └pose proof  (pf   :   Interpretation.   3.5%   3.5%       1    2.192s
─synthesize ----------------------------   0.0%   4.5%       1    2.800s
└IntegrationTestTemporaryMiscCommon.do_r   0.0%   4.3%       1    2.720s
└change G' -----------------------------   4.2%   4.2%       1    2.652s

src/Specific/solinas32_2e255m765_13limbs/femul (real: 178.02, user: 176.01, sys: 0.38, mem: 1713136 ko)
```
and
```
 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─Pipeline.refine_reflectively_gen ------   0.0%  95.8%       1   48.612s
 ├─ReflectiveTactics.do_reflective_pipel  -0.0%  89.1%       1   45.204s
 │└ReflectiveTactics.solve_side_conditio   0.0%  88.8%       1   45.040s
 │ ├─ReflectiveTactics.do_reify --------   0.0%  50.7%       1   25.720s
 │ │└Reify.Reify_rhs_gen ---------------   1.4%  50.1%       1   25.400s
 │ │ ├─Reify.do_reify_abs_goal ---------  37.3%  37.5%       2   19.012s
 │ │ │└Reify.do_reifyf_goal ------------  36.6%  36.9%     108    9.628s
 │ │ │└eexact --------------------------  11.4%  11.4%     108    0.072s
 │ │ ├─prove_interp_compile_correct ----   0.0%   2.9%       1    1.492s
 │ │ │└rewrite ?EtaInterp.InterpExprEta    2.6%   2.6%       1    1.344s
 │ │ └─rewrite H -----------------------   2.9%   2.9%       1    1.460s
 │ └─ReflectiveTactics.solve_post_reifie   0.1%  38.1%       1   19.320s
 │  └UnifyAbstractReflexivity.unify_tran  30.2%  35.2%       8    7.924s
 │  └unify (constr) (constr) -----------   4.2%   4.2%       6    1.060s
 └─Glue.refine_to_reflective_glue' -----   0.0%   6.7%       1    3.408s
  └Glue.zrange_to_reflective -----------   0.0%   6.2%       1    3.140s
  └Glue.zrange_to_reflective_goal ------   1.3%   4.7%       1    2.388s
  └pose proof  (pf   :   Interpretation.   3.2%   3.2%       1    1.644s
─synthesize ----------------------------   0.0%   4.2%       1    2.136s
└IntegrationTestTemporaryMiscCommon.do_r   0.0%   4.1%       1    2.072s
└change G' -----------------------------   4.0%   4.0%       1    2.008s

src/Specific/solinas32_2e255m765_12limbs/femul (real: 153.02, user: 151.06, sys: 0.37, mem: 1557920 ko)
```

1 files changed, 5 insertions, 12 deletions

diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 0b9d364dd..645f81634 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -11,6 +11,7 @@
 (** ** Preamble *)
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Intros.
 Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Compilers.WfReflective.
 Require Import Crypto.Compilers.RenameBinders.
@@ -143,16 +144,7 @@ Ltac boundedness_side_condition_solver :=
          end;
   try abstract ring.
 Ltac handle_boundedness_side_condition :=
-  (** TODO: This next bit, with repeat intros [? ?], could be done
-        with a single [apply], if we make the right lemma.  We should
-        write that lemma. *)
-  cbv [PointedProp.to_prop Syntax.interp_flat_type Syntax.interp_base_type Syntax.domain Syntax.codomain];
-  repeat match goal with
-         | [ |- forall x : _ * _, _ ]
-           => let a := fresh in let b := fresh in intros [a b]; revert a b
-         | [ |- forall x, _ ]
-           => let x := fresh "x" in intro x
-         end;
+  post_intro_interp_flat_type_intros;
   cbv [id
          fst snd
          InterpSideConditions Compilers.InterpSideConditions.InterpSideConditions interp_side_conditions interpf_side_conditions interpf_side_conditions_gen
@@ -162,7 +154,7 @@ Ltac handle_boundedness_side_condition :=
          Syntax.Zinterp_op
          SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartValf SmartMap.SmartFlatTypeMapInterp2
          Syntax.cast_const Syntax.ZToInterp Syntax.interpToZ];
-  cbv [PointedProp.and_pointed_Prop];
+  cbv [PointedProp.and_pointed_Prop PointedProp.to_prop];
   try match goal with
       | [ |- True ] => exact I
       end;
@@ -250,7 +242,7 @@ Section with_round_up_list.
       Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v';
       (** ** side conditions (boundedness) *)
       Hv1 : Bounds.is_bounded_by input_bounds (cast_back_flat_const v');
-      Hv2 : forall v, PointedProp.to_prop (InterpSideConditions e_pre_pkg v);
+      Hv2 : intros_interp_flat_type_Prop (fun v => PointedProp.to_prop (InterpSideConditions e_pre_pkg v));
     }.
 
   Definition PipelineCorrect
@@ -273,6 +265,7 @@ Section with_round_up_list.
     symmetry in Hpost_correct.
     subst; cbv [proj1_sig] in *.
     rewrite eq_InterpEta, <- Hrexpr.
+    pose proof (introsP_interp_flat_type Hv2) as Hv2'.
     eapply PostWfPipelineCorrect in Hpost_correct; [ | solve [ eauto ].. ].
     rewrite !@InterpPreWfPipeline in Hpost_correct.
     unshelve eapply relax_output_bounds; try eassumption; [].