Switch to a faster way of proving wf

By keeping more data in the reified side-condition, we can reflectively
replace all side conditions of the form [x = y] with [x = x], and check
via vm_cast that this does not change the side condition.  This is
empirically a cheap check, and since we can prove that all propositions
become true under this sort of replacement, we get most of our proof for
free.

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
12m15.26s | Total                                                                  | 12m34.17s || -0m18.90s
-----------------------------------------------------------------------------------------------------------
0m06.92s  | Specific/GF25519Reflective/Reified/Mul                                 | 0m14.58s  || -0m07.66s
0m05.99s  | Specific/GF25519Reflective/Reified/Freeze                              | 0m10.74s  || -0m04.75s
   N/A    | Reflection/WfRelReflective                                             | 0m04.05s  || -0m04.04s
0m02.00s  | Reflection/WfReflective                                                | 0m04.05s  || -0m02.04s
1m17.14s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 1m16.12s  || +0m01.01s
1m32.08s  | Test/Curve25519SpecTestVectors                                         | 1m32.06s  || +0m00.01s
0m40.68s  | ModularArithmetic/Conversion                                           | 0m40.54s  || +0m00.14s
0m34.50s  | Spec/Ed25519                                                           | 0m34.74s  || -0m00.24s
0m30.28s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m30.33s  || -0m00.04s
0m29.06s  | Experiments/Ed25519                                                    | 0m29.43s  || -0m00.37s
0m23.05s  | Experiments/MontgomeryCurve                                            | 0m22.85s  || +0m00.19s
0m22.37s  | Specific/GF25519                                                       | 0m22.28s  || +0m00.08s
0m22.06s  | ModularArithmetic/Pow2BaseProofs                                       | 0m22.08s  || -0m00.01s
0m20.17s  | Algebra                                                                | 0m20.11s  || +0m00.06s
0m17.10s  | EdDSARepChange                                                         | 0m17.21s  || -0m00.10s
0m16.85s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m17.03s  || -0m00.17s
0m13.86s  | Util/ZUtil                                                             | 0m13.72s  || +0m00.13s
0m09.98s  | Testbit                                                                | 0m10.03s  || -0m00.04s
0m08.94s  | [require-in-module,deprecated]
src/Assembly/GF25519                    | 0m09.08s  || -0m00.14s
0m08.81s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m08.71s  || +0m00.09s
0m08.45s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m08.46s  || -0m00.01s
0m08.39s  | Specific/GF25519BoundedCommonWord                                      | 0m08.41s  || -0m00.01s
0m08.39s  | Specific/GF1305                                                        | 0m08.44s  || -0m00.04s
0m08.35s  | Encoding/PointEncoding                                                 | 0m08.41s  || -0m00.06s
0m08.22s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.25s  || -0m00.02s
0m07.76s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m07.77s  || -0m00.00s
0m07.18s  | Specific/GF25519BoundedCommon                                          | 0m07.34s  || -0m00.16s
0m06.80s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m07.03s  || -0m00.23s
0m06.10s  | Bedrock/Word                                                           | 0m06.08s  || +0m00.01s
0m05.45s  | Specific/SC25519                                                       | 0m05.44s  || +0m00.00s
0m05.44s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m05.49s  || -0m00.04s
0m05.40s  | Util/ListUtil                                                          | 0m05.38s  || +0m00.02s
0m05.32s  | Experiments/GenericFieldPow                                            | 0m05.31s  || +0m00.01s
0m04.81s  | WeierstrassCurve/Pre                                                   | 0m04.82s  || -0m00.01s
0m04.76s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m04.84s  || -0m00.08s
0m04.40s  | Reflection/Z/Interpretations                                           | 0m04.48s  || -0m00.08s
0m04.22s  | Reflection/LinearizeWf                                                 | 0m04.21s  || +0m00.00s
0m03.92s  | BaseSystemProofs                                                       | 0m03.88s  || +0m00.04s
0m03.91s  | Assembly/GF25519BoundedInstantiation                                   | 0m03.78s  || +0m00.13s
0m03.83s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m03.90s  || -0m00.06s
0m03.67s  | ModularArithmetic/Tutorial                                             | 0m03.53s  || +0m00.14s
0m03.56s  | CompleteEdwardsCurve/Pre                                               | 0m03.50s  || +0m00.06s
0m03.36s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.30s  || +0m00.06s
0m03.03s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m03.12s  || -0m00.09s
0m02.92s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m02.90s  || +0m00.02s
0m02.89s  | ModularArithmetic/ZBoundedZ                                            | 0m02.84s  || +0m00.05s
0m02.86s  | Specific/GF25519Reflective/Reified/CarrySub                            | 0m03.15s  || -0m00.29s
0m02.85s  | Encoding/PointEncodingPre                                              | 0m02.87s  || -0m00.02s
0m02.62s  | Assembly/State                                                         | 0m02.71s  || -0m00.08s
0m02.61s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m02.60s  || +0m00.00s
0m02.54s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m02.60s  || -0m00.06s
0m02.53s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m02.50s  || +0m00.02s
0m02.52s  | Specific/GF25519Reflective/Reified/CarryOpp                            | 0m03.00s  || -0m00.48s
0m02.51s  | Specific/GF25519Reflective/Reified/CarryAdd                            | 0m02.50s  || +0m00.00s
0m02.38s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.34s  || +0m00.04s
0m02.28s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.30s  || -0m00.02s
0m02.16s  | Specific/FancyMachine256/Montgomery                                    | 0m02.07s  || +0m00.09s
0m02.13s  | Specific/FancyMachine256/Barrett                                       | 0m02.18s  || -0m00.05s
0m01.93s  | Reflection/WfProofs                                                    | 0m01.89s  || +0m00.04s
0m01.84s  | Assembly/Evaluables                                                    | 0m02.00s  || -0m00.15s
0m01.84s  | Specific/FancyMachine256/Core                                          | 0m01.91s  || -0m00.06s
0m01.84s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m01.79s  || +0m00.05s
0m01.79s  | Specific/GF25519Bounded                                                | 0m01.74s  || +0m00.05s
0m01.79s  | Specific/GF25519Reflective/Reified/Sub                                 | 0m01.66s  || +0m00.13s
0m01.78s  | Specific/GF25519Reflective/Reified/Pack                                | 0m01.80s  || -0m00.02s
0m01.76s  | Reflection/InlineWf                                                    | 0m01.69s  || +0m00.07s
0m01.68s  | Specific/GF25519Reflective/Reified/Unpack                              | 0m01.71s  || -0m00.03s
0m01.55s  | Reflection/InlineInterp                                                | 0m01.58s  || -0m00.03s
0m01.53s  | ModularArithmetic/BarrettReduction/Z                                   | 0m01.55s  || -0m00.02s
0m01.51s  | Specific/GF25519Reflective/Reified/Add                                 | 0m01.29s  || +0m00.21s
0m01.48s  | Specific/GF25519Reflective/Reified/Opp                                 | 0m01.49s  || -0m00.01s
0m01.47s  | Assembly/WordizeUtil                                                   | 0m01.52s  || -0m00.05s
0m01.45s  | Assembly/Compile                                                       | 0m01.45s  || +0m00.00s
0m01.43s  | Reflection/TestCase                                                    | 0m01.44s  || -0m00.01s
0m01.42s  | Specific/GF25519Reflective/Reified/GeModulus                           | 0m01.34s  || +0m00.07s
0m01.41s  | Util/NatUtil                                                           | 0m01.39s  || +0m00.02s
0m01.32s  | Assembly/Bounds                                                        | 0m01.33s  || -0m00.01s
0m01.31s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m01.27s  || +0m00.04s
0m01.18s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.11s  || +0m00.06s
0m01.17s  | BaseSystem                                                             | 0m01.16s  || +0m00.01s
0m01.15s  | Assembly/Conversions                                                   | 0m01.12s  || +0m00.02s
0m01.08s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.11s  || -0m00.03s
0m01.00s  | Assembly/Pipeline                                                      | 0m01.00s  || +0m00.00s
0m00.99s  | Util/WordUtil                                                          | 0m01.07s  || -0m00.08s
0m00.98s  | Assembly/HL                                                            | 0m01.04s  || -0m00.06s
0m00.98s  | Assembly/LL                                                            | 0m01.00s  || -0m00.02s
0m00.98s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.91s  || +0m00.06s
0m00.97s  | Assembly/PhoasCommon                                                   | 0m00.89s  || +0m00.07s
0m00.92s  | Util/NumTheoryUtil                                                     | 0m00.91s  || +0m00.01s
0m00.87s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.80s  || +0m00.06s
0m00.83s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m00.86s  || -0m00.03s
0m00.78s  | Specific/GF25519Reflective/Reified                                     | 0m00.68s  || +0m00.09s
0m00.78s  | Util/IterAssocOp                                                       | 0m00.78s  || +0m00.00s
0m00.77s  | Specific/GF25519Reflective/Common                                      | 0m00.70s  || +0m00.07s
0m00.76s  | Assembly/QhasmEvalCommon                                               | 0m00.78s  || -0m00.02s
0m00.75s  | Util/PartiallyReifiedProp                                              | 0m00.74s  || +0m00.01s
0m00.72s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.62s  || +0m00.09s
0m00.72s  | Util/Tuple                                                             | 0m00.72s  || +0m00.00s
0m00.66s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.64s  || +0m00.02s
0m00.63s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.63s  || +0m00.00s
0m00.62s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.70s  || -0m00.07s
0m00.61s  | Util/AdditionChainExponentiation                                       | 0m00.60s  || +0m00.01s
0m00.61s  | Reflection/LinearizeInterp                                             | 0m00.51s  || +0m00.09s
0m00.60s  | Encoding/ModularWordEncodingPre                                        | 0m00.58s  || +0m00.02s
0m00.60s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.61s  || -0m00.01s
0m00.60s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.61s  || -0m00.01s
0m00.60s  | Spec/EdDSA                                                             | 0m00.60s  || +0m00.00s
0m00.58s  | Reflection/InterpWfRel                                                 | 0m00.57s  || +0m00.01s
0m00.57s  | Reflection/WfReflectiveGen                                             | 0m00.60s  || -0m00.03s
0m00.56s  | BoundedArithmetic/Interface                                            | 0m00.65s  || -0m00.08s
0m00.56s  | Spec/ModularWordEncoding                                               | 0m00.72s  || -0m00.15s
0m00.56s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.62s  || -0m00.05s
0m00.56s  | BoundedArithmetic/X86ToZLike                                           | 0m00.63s  || -0m00.06s
0m00.55s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.54s  || +0m00.01s
0m00.52s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.52s  || +0m00.00s
0m00.51s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.42s  || +0m00.09s
0m00.50s  | Assembly/StringConversion                                              | 0m00.54s  || -0m00.04s
0m00.50s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.49s  || +0m00.01s
0m00.50s  | ModularArithmetic/ZBounded                                             | 0m00.51s  || -0m00.01s
0m00.49s  | Assembly/Qhasm                                                         | 0m00.53s  || -0m00.04s
0m00.49s  | Reflection/Z/Syntax                                                    | 0m00.50s  || -0m00.01s
0m00.48s  | BoundedArithmetic/Double/Core                                          | 0m00.47s  || +0m00.01s
0m00.48s  | Reflection/Z/Reify                                                     | 0m00.41s  || +0m00.07s
0m00.48s  | ModularArithmetic/Pre                                                  | 0m00.48s  || +0m00.00s
0m00.48s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.46s  || +0m00.01s
0m00.47s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.62s  || -0m00.15s
0m00.47s  | Reflection/InterpWf                                                    | 0m00.47s  || +0m00.00s
0m00.47s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.47s  || +0m00.00s
0m00.46s  | Assembly/QhasmUtil                                                     | 0m00.45s  || +0m00.01s
0m00.46s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.49s  || -0m00.02s
0m00.46s  | Reflection/CommonSubexpressionElimination                              | 0m00.44s  || +0m00.02s
0m00.45s  | Util/Decidable                                                         | 0m00.54s  || -0m00.09s
0m00.44s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.42s  || +0m00.02s
0m00.44s  | Reflection/Conversion                                                  | 0m00.42s  || +0m00.02s
0m00.44s  | Reflection/InterpProofs                                                | 0m00.45s  || -0m00.01s
0m00.44s  | BoundedArithmetic/Eta                                                  | 0m00.39s  || +0m00.04s
0m00.42s  | Reflection/MapInterpWf                                                 | 0m00.41s  || +0m00.01s
0m00.42s  | Reflection/Syntax                                                      | 0m00.44s  || -0m00.02s
0m00.42s  | Spec/WeierstrassCurve                                                  | 0m00.43s  || -0m00.01s
0m00.42s  | Reflection/Named/NameUtil                                              | 0m00.35s  || +0m00.07s
0m00.42s  | BoundedArithmetic/StripCF                                              | 0m00.48s  || -0m00.06s
0m00.42s  | Reflection/Named/RegisterAssign                                        | 0m00.41s  || +0m00.01s
0m00.42s  | Reflection/InputSyntax                                                 | 0m00.42s  || +0m00.00s
0m00.42s  | Spec/MxDH                                                              | 0m00.40s  || +0m00.01s
0m00.41s  | Reflection/CountLets                                                   | 0m00.36s  || +0m00.04s
0m00.41s  | Reflection/Named/EstablishLiveness                                     | 0m00.36s  || +0m00.04s
0m00.40s  | ModularArithmetic/Pow2Base                                             | 0m00.42s  || -0m00.01s
0m00.39s  | Reflection/MapInterp                                                   | 0m00.35s  || +0m00.04s
0m00.39s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.45s  || -0m00.06s
0m00.39s  | Reflection/Named/Syntax                                                | 0m00.42s  || -0m00.02s
0m00.38s  | Reflection/FilterLive                                                  | 0m00.35s  || +0m00.03s
0m00.38s  | Spec/CompleteEdwardsCurve                                              | 0m00.44s  || -0m00.06s
0m00.38s  | Reflection/Named/DeadCodeElimination                                   | 0m00.36s  || +0m00.02s
0m00.38s  | Reflection/Linearize                                                   | 0m00.38s  || +0m00.00s
0m00.37s  | Reflection/Inline                                                      | 0m00.38s  || -0m00.01s
0m00.37s  | ModularArithmetic/Montgomery/Z                                         | 0m00.36s  || +0m00.01s
0m00.37s  | Reflection/WfRel                                                       | 0m00.37s  || +0m00.00s
0m00.36s  | Assembly/QhasmCommon                                                   | 0m00.31s  || +0m00.04s
0m00.35s  | Tactics/Algebra_syntax/Nsatz                                           | 0m00.37s  || -0m00.02s
0m00.35s  | Spec/ModularArithmetic                                                 | 0m00.36s  || -0m00.01s
0m00.34s  | Reflection/Named/Compile                                               | 0m00.36s  || -0m00.01s
0m00.34s  | Reflection/Named/ContextOn                                             | 0m00.34s  || +0m00.00s
0m00.34s  | Reflection/Reify                                                       | 0m00.35s  || -0m00.00s
0m00.28s  | Bedrock/Nomega                                                         | 0m00.28s  || +0m00.00s
0m00.24s  | ModularArithmetic/ModularBaseSystemListZOperations                     | 0m00.26s  || -0m00.02s
0m00.21s  | Util/Sum                                                               | 0m00.24s  || -0m00.03s
0m00.19s  | Util/CaseUtil                                                          | 0m00.22s  || -0m00.03s
0m00.18s  | Experiments/ExtrHaskellNats                                            | 0m00.17s  || +0m00.00s
0m00.13s  | Util/Relations                                                         | 0m00.14s  || -0m00.01s
0m00.10s  | Util/Option                                                            | 0m00.14s  || -0m00.04s
0m00.09s  | Util/PointedProp                                                       | 0m00.08s  || +0m00.00s
0m00.08s  | Util/Sigma                                                             | 0m00.10s  || -0m00.02s
0m00.08s  | Util/LetIn                                                             | 0m00.04s  || +0m00.04s
0m00.05s  | Util/HProp                                                             | 0m00.04s  || +0m00.01s
0m00.05s  | Util/Tactics                                                           | 0m00.04s  || +0m00.01s
0m00.05s  | Util/Equality                                                          | 0m00.04s  || +0m00.01s
0m00.04s  | Util/Prod                                                              | 0m00.05s  || -0m00.01s
0m00.04s  | Util/AutoRewrite                                                       | 0m00.04s  || +0m00.00s
0m00.03s  | Util/Unit                                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Spec/Encoding                                                          | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Logic                                                             | 0m00.03s  || +0m00.00s
0m00.02s  | Tactics/VerdiTactics                                                   | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Notations                                                         | 0m00.02s  || +0m00.00s
0m00.02s  | Encoding/EncodingTheorems                                              | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Isomorphism                                                       | 0m00.02s  || +0m00.00s
0m00.02s  | Util/GlobalSettings                                                    | 0m00.02s  || +0m00.00s
0m00.02s  | Util/FixCoqMistakes                                                    | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Bool                                                              | 0m00.02s  || +0m00.00s

5 files changed, 131 insertions, 291 deletions

diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
index 844fea592..a7e2146a6 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Reflection/TestCase.v
@@ -96,23 +96,20 @@ Lemma base_type_eq_semidec_is_dec : forall t1 t2,
 Proof.
   intros t1 t2; destruct t1, t2; simpl; intros; congruence.
 Qed.
-Definition op_beq t1 tR : op t1 tR -> op t1 tR -> option pointed_Prop
-  := fun x y => match x, y with
-             | Add, Add => Some trivial
-             | Add, _ => None
-             | Mul, Mul => Some trivial
-             | Mul, _ => None
-             | Sub, Sub => Some trivial
-             | Sub, _ => None
-             end.
+Definition op_beq t1 tR : op t1 tR -> op t1 tR -> reified_Prop
+  := fun x y => match x, y return bool with
+                | Add, Add => true
+                | Add, _ => false
+                | Mul, Mul => true
+                | Mul, _ => false
+                | Sub, Sub => true
+                | Sub, _ => false
+                end.
 Lemma op_beq_bl t1 tR (x y : op t1 tR)
-  : match op_beq t1 tR x y with
-    | Some p => to_prop p
-    | None => False
-    end -> x = y.
+  : to_prop (op_beq t1 tR x y) -> x = y.
 Proof.
   destruct x; simpl;
-    refine match y with Add => _ | _ => _ end; tauto.
+    refine match y with Add => _ | _ => _ end; simpl; tauto.
 Qed.
 
 Ltac reflect_Wf := WfReflective.reflect_Wf base_type_eq_semidec_is_dec op_beq_bl.
diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v
index d68ed53ac..8a8eef38f 100644
--- a/src/Reflection/WfReflective.v
+++ b/src/Reflection/WfReflective.v
@@ -45,13 +45,13 @@
 
     - [op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y)
       -> x = y] for some [op_beq : forall t1 tR, op t1 tR -> op t1 tR
-      -> option pointed_Prop] *)
+      -> reified_Prop] *)
 
 Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.WfReflectiveGen.
 Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
-Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *)
+Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *)
 Require Export Crypto.Util.FixCoqMistakes.
 
 
@@ -74,8 +74,8 @@ Section language.
       [pointed_Prop] internally because we need to talk about equality
       of things of type [var t], for [var : base_type_code -> Type].
       It does not hurt to allow extra generality in [op_beq]. *)
-  Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop).
-  Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y).
+  Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> reified_Prop).
+  Context (op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y).
   Context {var1 var2 : base_type_code -> Type}.
 
   Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing).
@@ -90,8 +90,8 @@ Section language.
   Local Notation exprf := (@exprf base_type_code interp_base_type op).
   Local Notation expr := (@expr base_type_code interp_base_type op).
   Local Notation duplicate_type := (@duplicate_type base_type_code var1 var2).
-  Local Notation reflect_wffT := (@reflect_wffT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2).
-  Local Notation reflect_wfT := (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2).
+  Local Notation reflect_wffT := (@reflect_wffT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2).
+  Local Notation reflect_wfT := (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2).
   Local Notation flat_type_eq_semidec_transparent := (@flat_type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent).
   Local Notation preflatten_binding_list2 := (@preflatten_binding_list2 base_type_code base_type_eq_semidec_transparent var1 var2).
   Local Notation type_eq_semidec_transparent := (@type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent).
@@ -105,25 +105,25 @@ Section language.
 
   Local Ltac handle_op_beq_correct :=
     repeat match goal with
-           | [ H : op_beq ?t1 ?tR ?x ?y = _ |- _ ]
-             => let H' := fresh in
-               pose proof (op_beq_bl t1 tR x y) as H'; rewrite H in H'; clear H
+           | [ H : to_prop (op_beq ?t1 ?tR ?x ?y) |- _ ]
+             => apply op_beq_bl in H
            end.
   Local Ltac t_step :=
     match goal with
-    | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, WfReflectiveGen.preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in *
+    | [ |- True ] => exact I
+    | _ => progress cbv beta delta [eq_type_and_var op_beq' flatten_binding_list2 WfReflectiveGen.preflatten_binding_list2 option_map eq_semidec_and_gen] in *
     | _ => progress simpl in *
-    | _ => progress break_match
-    | [ H : interp_flat_type_rel_pointwise2 (fun _ => eq) _ _ |- _ ]
-      => apply interp_flat_type_rel_pointwise2_eq in H
     | _ => progress subst
+    | _ => progress break_innermost_match_step
     | _ => progress inversion_option
-    | _ => progress inversion_pointed_Prop
+    | _ => progress inversion_prod
+    | _ => progress inversion_reified_Prop
     | _ => congruence
     | _ => tauto
     | _ => progress intros
     | _ => progress handle_op_beq_correct
     | _ => progress specialize_by tauto
+    | [ v : ex _ |- _ ] => destruct v
     | [ v : sigT _ |- _ ] => destruct v
     | [ v : prod _ _ |- _ ] => destruct v
     | [ H : forall x x', _ |- wff (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ]
@@ -131,6 +131,7 @@ Section language.
     | [ H : forall x x', _ |- wf (existT _ _ (?x1, ?x2) :: _)%list _ _ ]
       => specialize (H x1 x2)
     | [ H : and _ _ |- _ ] => destruct H
+    | [ H : to_prop (_ /\ _) |- _ ] => apply to_prop_and_reified_Prop in H; destruct H
     | [ H : context[duplicate_type (_ ++ _)%list] |- _ ]
       => rewrite duplicate_type_app in H
     | [ H : context[List.length (duplicate_type _)] |- _ ]
@@ -144,25 +145,28 @@ Section language.
     | [ H : base_type_eq_semidec_transparent _ _ = None |- False ] => eapply duplicate_type_not_in; eassumption
     | [ H : List.nth_error _ _ = Some _ |- _ ] => apply List.nth_error_In in H
     | [ H : List.In _ (duplicate_type _) |- _ ] => eapply duplicate_type_in in H; [ | eassumption.. ]
-    | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_match
+    | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_innermost_match
     | [ |- wff _ _ _ ] => constructor
     | [ |- wf _ _ _ ] => constructor
-    | _ => progress unfold and_pointed_Prop in *
+    | _ => progress unfold and_reified_Prop in *
     end.
   Local Ltac t := repeat t_step.
   Fixpoint reflect_wff (G : list (sigT (fun t => var1 t * var2 t)%type))
            {t1 t2 : flat_type}
            (e1 : @exprf (fun t => nat * var1 t)%type t1) (e2 : @exprf (fun t => nat * var2 t)%type t2)
            {struct e1}
-    : match reflect_wffT (duplicate_type G) e1 e2, flat_type_eq_semidec_transparent t1 t2 with
-      | Some reflective_obligation, Some p
+    : let reflective_obligation := reflect_wffT (duplicate_type G) e1 e2 in
+      match flat_type_eq_semidec_transparent t1 t2 with
+      | Some p
         => to_prop reflective_obligation
           -> @wff base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2)
-      | _, _ => True
+      | None => True
       end.
   Proof.
+    cbv zeta.
     destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ],
-                   e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ exact I ];
+                   e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl;
+      try solve [ break_match; solve [ exact I | intros [] ] ];
       [ clear reflect_wff
       | clear reflect_wff
       | specialize (reflect_wff G _ _ args args')
@@ -187,11 +191,12 @@ Section language.
   Fixpoint reflect_wf (G : list (sigT (fun t => var1 t * var2 t)%type))
            {t1 t2 : type}
            (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2)
-    : match reflect_wfT (duplicate_type G) e1 e2, type_eq_semidec_transparent t1 t2 with
-      | Some reflective_obligation, Some p
+    : let reflective_obligation := reflect_wfT (duplicate_type G) e1 e2 in
+      match type_eq_semidec_transparent t1 t2 with
+      | Some p
         => to_prop reflective_obligation
           -> @wf base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ expr (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2)
-      | _, _ => True
+      | None => True
       end.
   Proof.
     destruct e1 as [ t1 e1 | tx tR f ],
@@ -219,15 +224,15 @@ Section Wf.
           (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2))
           (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2)
           (op : flat_type base_type_code -> flat_type base_type_code -> Type)
-          (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop)
-          (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y)
+          (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> reified_Prop)
+          (op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y)
           {t : type base_type_code}
           (e : @Expr base_type_code interp_base_type op t).
 
   (** Leads to smaller proofs, but is less generally applicable *)
   Theorem reflect_Wf_unnatize
     : (forall var1 var2,
-          prop_of_option (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2 nil t t (e _) (e _)))
+          to_prop (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2 nil t t (e _) (e _)))
       -> Wf (fun var => unnatize_expr 0 (e (fun t => (nat * var t)%type))).
   Proof.
     intros H var1 var2; specialize (H var1 var2).
@@ -241,7 +246,7 @@ Section Wf.
   Theorem reflect_Wf
     : (forall var1 var2,
           unnatize_expr 0 (e (fun t => (nat * var1 t)%type)) = e _
-          /\ prop_of_option (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => eq) op_beq var1 var2 nil t t (e _) (e _)))
+          /\ to_prop (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2 nil t t (e _) (e _)))
       -> Wf e.
   Proof.
     intros H var1 var2.
@@ -256,8 +261,22 @@ Ltac generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl :=
   | [ |- @Wf ?base_type_code ?interp_base_type ?op ?t ?e ]
     => generalize (@reflect_Wf_unnatize base_type_code interp_base_type _ base_type_eq_semidec_is_dec op _ op_beq_bl t e)
   end.
-Ltac use_reflect_Wf := vm_compute; let H := fresh in intro H; apply H; clear H.
-Ltac fin_reflect_Wf := repeat constructor.
+Ltac use_reflect_Wf :=
+  let H := fresh in
+  intro H;
+  lazymatch type of H with
+  | ?A -> ?B
+    => cut A
+  end;
+  [ abstract vm_cast_no_check H
+  | clear H ].
+Ltac fin_reflect_Wf :=
+  intros;
+  lazymatch goal with
+  | [ |- to_prop ?P ]
+    => replace P with (trueify P) by abstract vm_cast_no_check (eq_refl P)
+  end;
+  apply trueify_true.
 (** The tactic [reflect_Wf] is the main tactic of this file, used to
     prove [Syntax.Wf] goals *)
 Ltac reflect_Wf base_type_eq_semidec_is_dec op_beq_bl :=
diff --git a/src/Reflection/WfReflectiveGen.v b/src/Reflection/WfReflectiveGen.v
index 4935134d8..0d961ec97 100644
--- a/src/Reflection/WfReflectiveGen.v
+++ b/src/Reflection/WfReflectiveGen.v
@@ -50,7 +50,7 @@
 Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
-Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *)
+Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *)
 Require Export Crypto.Util.FixCoqMistakes.
 
 
@@ -67,15 +67,15 @@ Section language.
           (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2))
           (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2)
           (op : flat_type base_type_code -> flat_type base_type_code -> Type)
-          (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop).
+          (R : forall t, interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> reified_Prop).
   (** In practice, semi-deciding equality of operators should either
       return [Some trivial] or [None], and not make use of the
       generality of [pointed_Prop].  However, we need to use
       [pointed_Prop] internally because we need to talk about equality
       of things of type [var t], for [var : base_type_code -> Type].
       It does not hurt to allow extra generality in [op_beq]. *)
-  Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop).
-  Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y).
+  Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> reified_Prop).
+  Context (op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y).
   Context {var1 var2 : base_type_code -> Type}.
 
   Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing).
@@ -151,13 +151,13 @@ Section language.
     { rewrite base_type_eq_semidec_transparent_refl; rewrite_hyp !*; reflexivity. }
   Qed.
 
-  Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : option pointed_Prop
+  Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : reified_Prop
     := match flat_type_eq_semidec_transparent t1 t1', flat_type_eq_semidec_transparent tR tR' with
        | Some p, Some q
          => match p in (_ = t1'), q in (_ = tR') return op t1' tR' -> _ with
            | eq_refl, eq_refl => fun y => op_beq _ _ x y
            end y
-       | _, _ => None
+       | _, _ => rFalse
        end.
 
   (** While [Syntax.wff] is parameterized over a list of [sigT (fun t
@@ -178,27 +178,27 @@ Section language.
         about [Syntax.wff] itself.  *)
 
   Definition eq_semidec_and_gen {T} (semidec : forall x y : T, option (x = y))
-             (t t' : T) (f g : T -> Type) (R : forall t, f t -> g t -> Prop)
+             (t t' : T) (f g : T -> Type) (R : forall t, f t -> g t -> reified_Prop)
              (x : f t) (x' : g t')
-    : option pointed_Prop
+    : reified_Prop
     := match semidec t t' with
        | Some p
-         => Some (inject (R _ (eq_rect _ f x _ p) x'))
-       | None => None
+         => R _ (eq_rect _ f x _ p) x'
+       | None => rFalse
        end.
 
   (* Here is where we use the generality of [pointed_Prop], to say
      that two things of type [var1] are equal, and two things of type
      [var2] are equal. *)
-  Definition eq_type_and_var : sigT eP -> sigT eP -> option pointed_Prop
+  Definition eq_type_and_var : sigT eP -> sigT eP -> reified_Prop
     := fun x y => (eq_semidec_and_gen
-                  base_type_eq_semidec_transparent _ _ var1 var1 (fun _ => eq) (fst (projT2 x)) (fst (projT2 y))
+                  base_type_eq_semidec_transparent _ _ var1 var1 (fun _ => rEq) (fst (projT2 x)) (fst (projT2 y))
                 /\ eq_semidec_and_gen
-                     base_type_eq_semidec_transparent _ _ var2 var2 (fun _ => eq) (snd (projT2 x)) (snd (projT2 y)))%option_pointed_prop.
+                     base_type_eq_semidec_transparent _ _ var2 var2 (fun _ => rEq) (snd (projT2 x)) (snd (projT2 y)))%reified_prop.
   Definition rel_type_and_const (t t' : flat_type) (x : interp_flat_type1 t) (y : interp_flat_type2 t')
-    : option pointed_Prop
+    : reified_Prop
     := eq_semidec_and_gen
-         flat_type_eq_semidec_transparent _ _ interp_flat_type1 interp_flat_type2 (fun t => interp_flat_type_rel_pointwise2 R) x y.
+         flat_type_eq_semidec_transparent _ _ interp_flat_type1 interp_flat_type2 R x y.
 
   Definition duplicate_type (ls : list (sigT (fun t => var1 t * var2 t)%type)) : list (sigT eP)
     := List.map (fun v => existT eP (projT1 v, projT1 v) (projT2 v)) ls.
@@ -292,71 +292,61 @@ Section language.
            (e1 : @exprf1 (fun t => nat * var1 t)%type t1)
            (e2 : @exprf2 (fun t => nat * var2 t)%type t2)
            {struct e1}
-    : option pointed_Prop
-    := match e1, e2 return option _ with
+    : reified_Prop
+    := match e1, e2 with
        | Const t0 x, Const t1 y
          => match flat_type_eq_semidec_transparent t0 t1 with
-           | Some p => Some (inject (interp_flat_type_rel_pointwise2 R (eq_rect _ interp_flat_type1 x _ p) y))
-           | None => None
+           | Some p => R _ (eq_rect _ interp_flat_type1 x _ p) y
+           | None => rFalse
            end
-       | Const _ _, _ => None
+       | Const _ _, _ => rFalse
        | Var t0 x, Var t1 y
          => match beq_nat (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with
            | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y))
-           | _, _ => None
+           | _, _ => rFalse
            end
-       | Var _ _, _ => None
+       | Var _ _, _ => rFalse
        | Op t1 tR op args, Op t1' tR' op' args'
-         => match @reflect_wffT G t1 t1' args args', op_beq' t1 tR t1' tR' op op' with
-           | Some p, Some q => Some (p /\ q)%pointed_prop
-           | _, _ => None
-           end
-       | Op _ _ _ _, _ => None
+         => (@reflect_wffT G t1 t1' args args' /\ op_beq' t1 tR t1' tR' op op')%reified_prop
+       | Op _ _ _ _, _ => rFalse
        | LetIn tx ex tC eC, LetIn tx' ex' tC' eC'
-         => match @reflect_wffT G tx tx' ex ex', @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tC tC' with
-           | Some p, Some G0, Some _
-             => Some (p /\ inject (forall (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'),
-                                    match @reflect_wffT (G0 x x' ++ G)%list _ _
-                                                       (eC (snd (natize_interp_flat_type (List.length G) x)))
-                                                       (eC' (snd (natize_interp_flat_type (List.length G) x'))) with
-                                    | Some p => to_prop p
-                                    | None => False
-                                    end))
-           | _, _, _ => None
+         => let p := @reflect_wffT G tx tx' ex ex' in
+            match @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tC tC' with
+           | Some G0, Some _
+             => p
+                /\ (∀ (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'),
+                       @reflect_wffT (G0 x x' ++ G)%list _ _
+                                     (eC (snd (natize_interp_flat_type (List.length G) x)))
+                                     (eC' (snd (natize_interp_flat_type (List.length G) x'))))
+           | _, _ => rFalse
            end
-       | LetIn _ _ _ _, _ => None
+       | LetIn _ _ _ _, _ => rFalse
        | Pair tx ex ty ey, Pair tx' ex' ty' ey'
-         => match @reflect_wffT G tx tx' ex ex', @reflect_wffT G ty ty' ey ey' with
-           | Some p, Some q => Some (p /\ q)
-           | _, _ => None
-           end
-       | Pair _ _ _ _, _ => None
-       end%pointed_prop.
+         => @reflect_wffT G tx tx' ex ex' /\ @reflect_wffT G ty ty' ey ey'
+       | Pair _ _ _ _, _ => rFalse
+       end%reified_prop.
 
     Fixpoint reflect_wfT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type))
            {t1 t2 : type}
            (e1 : @expr1 (fun t => nat * var1 t)%type t1)
            (e2 : @expr2 (fun t => nat * var2 t)%type t2)
            {struct e1}
-    : option pointed_Prop
-    := match e1, e2 return option _ with
+    : reified_Prop
+    := match e1, e2 with
        | Return _ x, Return _ y
          => reflect_wffT G x y
-       | Return _ _, _ => None
+       | Return _ _, _ => rFalse
        | Abs tx tR f, Abs tx' tR' f'
          => match @flatten_binding_list2 tx tx', type_eq_semidec_transparent tR tR' with
            | Some G0, Some _
-             => Some (inject (forall (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'),
-                                match @reflect_wfT (G0 x x' ++ G)%list _ _
-                                                   (f (snd (natize_interp_flat_type (List.length G) x)))
-                                                   (f' (snd (natize_interp_flat_type (List.length G) x'))) with
-                                | Some p => to_prop p
-                                | None => False
-                                end))
-           | _, _ => None
+             => ∀ (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'),
+               @reflect_wfT (G0 x x' ++ G)%list _ _
+                            (f (snd (natize_interp_flat_type (List.length G) x)))
+                            (f' (snd (natize_interp_flat_type (List.length G) x')))
+           | _, _ => rFalse
            end
-       | Abs _ _ _, _ => None
-       end%pointed_prop.
+       | Abs _ _ _, _ => rFalse
+       end%reified_prop.
 End language.
 
 Global Arguments reflect_wffT {_ _ _} _ {op} R _ {var1 var2} G {t1 t2} _ _.
diff --git a/src/Reflection/WfRelReflective.v b/src/Reflection/WfRelReflective.v
deleted file mode 100644
index 0135f6afb..000000000
--- a/src/Reflection/WfRelReflective.v
+++ /dev/null
@@ -1,166 +0,0 @@
-(** * A reflective Version of [WfRel] proofs *)
-(** See [WfReflective.v] and [WfReflectiveGen.v] for comments. *)
-Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.WfRel.
-Require Import Crypto.Reflection.WfReflectiveGen.
-Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
-Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *)
-Require Export Crypto.Util.FixCoqMistakes.
-
-
-Section language.
-  (** To be able to optimize away so much of the [Syntax.wff] proof,
-      we must be able to decide a few things: equality of base types,
-      and equality of operator codes.  Since we will be casting across
-      the equality proofs of base types, we require that this
-      semi-decider give transparent proofs.  (This requirement is not
-      enforced, but it will block [vm_compute] when trying to use the
-      lemma in this file.) *)
-  Context (base_type_code : Type).
-  Context (interp_base_type1 interp_base_type2 : base_type_code -> Type).
-  Context (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)).
-  Context (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2).
-  Context (op : flat_type base_type_code -> flat_type base_type_code -> Type).
-  Context (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop).
-  (** In practice, semi-deciding equality of operators should either
-      return [Some trivial] or [None], and not make use of the
-      generality of [pointed_Prop].  However, we need to use
-      [pointed_Prop] internally because we need to talk about equality
-      of things of type [var t], for [var : base_type_code -> Type].
-      It does not hurt to allow extra generality in [op_beq]. *)
-  Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop).
-  Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y).
-  Context {var1 var2 : base_type_code -> Type}.
-
-  Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing).
-
-  (* convenience notations that fill in some arguments used across the section *)
-  Local Notation flat_type := (flat_type base_type_code).
-  Local Notation type := (type base_type_code).
-  Let Tbase := @Tbase base_type_code.
-  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
-  Local Notation interp_type1 := (interp_type interp_base_type1).
-  Local Notation interp_type2 := (interp_type interp_base_type2).
-  Local Notation interp_flat_type1 := (interp_flat_type interp_base_type1).
-  Local Notation interp_flat_type2 := (interp_flat_type interp_base_type2).
-  Local Notation exprf1 := (@exprf base_type_code interp_base_type1 op).
-  Local Notation exprf2 := (@exprf base_type_code interp_base_type2 op).
-  Local Notation expr1 := (@expr base_type_code interp_base_type1 op).
-  Local Notation expr2 := (@expr base_type_code interp_base_type2 op).
-  Local Notation duplicate_type := (@duplicate_type base_type_code var1 var2).
-  Local Notation reflect_wffT := (@reflect_wffT base_type_code interp_base_type1 interp_base_type2 base_type_eq_semidec_transparent op R op_beq var1 var2).
-  Local Notation reflect_wfT := (@reflect_wfT base_type_code interp_base_type1 interp_base_type2 base_type_eq_semidec_transparent op R op_beq var1 var2).
-  Local Notation flat_type_eq_semidec_transparent := (@flat_type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent).
-  Local Notation preflatten_binding_list2 := (@preflatten_binding_list2 base_type_code base_type_eq_semidec_transparent var1 var2).
-  Local Notation type_eq_semidec_transparent := (@type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent).
-
-  Local Ltac handle_op_beq_correct :=
-    repeat match goal with
-           | [ H : op_beq ?t1 ?tR ?x ?y = _ |- _ ]
-             => let H' := fresh in
-               pose proof (op_beq_bl t1 tR x y) as H'; rewrite H in H'; clear H
-           end.
-  Local Ltac t_step :=
-    match goal with
-    | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, WfReflectiveGen.preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in *
-    | _ => progress simpl in *
-    | _ => progress break_match
-    | _ => progress subst
-    | _ => progress inversion_option
-    | _ => progress inversion_pointed_Prop
-    | _ => congruence
-    | _ => tauto
-    | _ => progress intros
-    | _ => progress handle_op_beq_correct
-    | _ => progress specialize_by tauto
-    | [ v : sigT _ |- _ ] => destruct v
-    | [ v : prod _ _ |- _ ] => destruct v
-    | [ H : forall x x', _ |- rel_wff _ (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ]
-      => specialize (H x1 x2)
-    | [ H : forall x x', _ |- rel_wf _ (existT _ _ (?x1, ?x2) :: _)%list _ _ ]
-      => specialize (H x1 x2)
-    | [ H : and _ _ |- _ ] => destruct H
-    | [ H : context[duplicate_type (_ ++ _)%list] |- _ ]
-      => rewrite duplicate_type_app in H
-    | [ H : context[List.length (duplicate_type _)] |- _ ]
-      => rewrite duplicate_type_length in H
-    | [ H : context[List.length (_ ++ _)%list] |- _ ]
-      => rewrite List.app_length in H
-    | [ |- rel_wff _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ]
-      => erewrite length_natize_interp_flat_type1, length_natize_interp_flat_type2; eassumption
-    | [ |- rel_wf _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ]
-      => erewrite length_natize_interp_flat_type1, length_natize_interp_flat_type2; eassumption
-    | [ H : base_type_eq_semidec_transparent _ _ = None |- False ] => eapply duplicate_type_not_in; eassumption
-    | [ H : List.nth_error _ _ = Some _ |- _ ] => apply List.nth_error_In in H
-    | [ H : List.In _ (duplicate_type _) |- _ ] => eapply duplicate_type_in in H; [ | eassumption.. ]
-    | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_match
-    | [ |- rel_wff _ _ _ _ ] => constructor
-    | [ |- rel_wf _ _ _ _ ] => constructor
-    | _ => progress unfold and_pointed_Prop in *
-    end.
-  Local Ltac t := repeat t_step.
-  Fixpoint reflect_rel_wff (G : list (sigT (fun t => var1 t * var2 t)%type))
-           {t1 t2 : flat_type}
-           (e1 : @exprf1 (fun t => nat * var1 t)%type t1)
-           (e2 : @exprf2 (fun t => nat * var2 t)%type t2)
-           {struct e1}
-    : match reflect_wffT (duplicate_type G) e1 e2, flat_type_eq_semidec_transparent t1 t2 with
-      | Some reflective_obligation, Some p
-        => to_prop reflective_obligation
-          -> @rel_wff base_type_code interp_base_type1 interp_base_type2 op R var1 var2 G t2 (eq_rect _ exprf1 (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2)
-      | _, _ => True
-      end.
-  Proof.
-    destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ],
-                   e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ exact I ];
-      [ clear reflect_rel_wff
-      | clear reflect_rel_wff
-      | specialize (reflect_rel_wff G _ _ args args')
-      | pose proof (reflect_rel_wff G _ _ ex ex');
-        pose proof (fun x x'
-                    => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with
-                      | Some G0
-                        => reflect_rel_wff
-                            (G0 x x' ++ G)%list _ _
-                            (eC (snd (natize_interp_flat_type (length (duplicate_type G)) x)))
-                            (eC' (snd (natize_interp_flat_type (length (duplicate_type G)) x')))
-                      | None => I
-                      end);
-        clear reflect_rel_wff
-      | pose proof (reflect_rel_wff G _ _ ex ex'); pose proof (reflect_rel_wff G _ _ ey ey'); clear reflect_rel_wff ].
-    { t. }
-    { t. }
-    { t. }
-    { t. }
-    { t. }
-  Qed.
-  Fixpoint reflect_rel_wf (G : list (sigT (fun t => var1 t * var2 t)%type))
-           {t1 t2 : type}
-           (e1 : @expr1 (fun t => nat * var1 t)%type t1)
-           (e2 : @expr2 (fun t => nat * var2 t)%type t2)
-    : match reflect_wfT (duplicate_type G) e1 e2, type_eq_semidec_transparent t1 t2 with
-      | Some reflective_obligation, Some p
-        => to_prop reflective_obligation
-          -> @rel_wf base_type_code interp_base_type1 interp_base_type2 op R var1 var2 G t2 (eq_rect _ expr1 (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2)
-      | _, _ => True
-      end.
-  Proof.
-    destruct e1 as [ t1 e1 | tx tR f ],
-                   e2 as [ t2 e2 | tx' tR' f' ]; simpl; try solve [ exact I ];
-      [ clear reflect_rel_wf;
-        pose proof (@reflect_rel_wff G t1 t2 e1 e2)
-      | pose proof (fun x x'
-                    => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with
-                      | Some G0
-                        => reflect_rel_wf
-                            (G0 x x' ++ G)%list _ _
-                            (f (snd (natize_interp_flat_type (length (duplicate_type G)) x)))
-                            (f' (snd (natize_interp_flat_type (length (duplicate_type G)) x')))
-                      | None => I
-                      end);
-        clear reflect_rel_wf ].
-    { t. }
-    { t. }
-  Qed.
-End language.
diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v
index 2d31ec8e2..4b23cc274 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Reflection/Z/Syntax.v
@@ -4,7 +4,7 @@ Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
 Require Import Crypto.Util.Equality.
 Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.PartiallyReifiedProp.
 Export Syntax.Notations.
 
 Local Set Boolean Equality Schemes.
@@ -57,31 +57,31 @@ Proof.
   unfold base_type_eq_semidec_transparent; congruence.
 Qed.
 
-Definition op_beq t1 tR (f g : op t1 tR) : option pointed_Prop
-  := option_pointed_Prop_of_bool match f, g with
-                                 | Add, Add => true
-                                 | Add, _ => false
-                                 | Sub, Sub => true
-                                 | Sub, _ => false
-                                 | Mul, Mul => true
-                                 | Mul, _ => false
-                                 | Shl, Shl => true
-                                 | Shl, _ => false
-                                 | Shr, Shr => true
-                                 | Shr, _ => false
-                                 | Land, Land => true
-                                 | Land, _ => false
-                                 | Lor, Lor => true
-                                 | Lor, _ => false
-                                 | Neg, Neg => true
-                                 | Neg, _ => false
-                                 | Cmovne, Cmovne => true
-                                 | Cmovne, _ => false
-                                 | Cmovle, Cmovle => true
-                                 | Cmovle, _ => false
-                                 end.
+Definition op_beq t1 tR (f g : op t1 tR) : reified_Prop
+  := match f, g return bool with
+     | Add, Add => true
+     | Add, _ => false
+     | Sub, Sub => true
+     | Sub, _ => false
+     | Mul, Mul => true
+     | Mul, _ => false
+     | Shl, Shl => true
+     | Shl, _ => false
+     | Shr, Shr => true
+     | Shr, _ => false
+     | Land, Land => true
+     | Land, _ => false
+     | Lor, Lor => true
+     | Lor, _ => false
+     | Neg, Neg => true
+     | Neg, _ => false
+     | Cmovne, Cmovne => true
+     | Cmovne, _ => false
+     | Cmovle, Cmovle => true
+     | Cmovle, _ => false
+     end.
 
-Lemma op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y.
+Lemma op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y.
 Proof.
   intros ?? x; destruct x;
     intro y;