Add interp-correctness condition for rewriter

The NBE-rewrite rules are proven correct.  The arith and fancy rewrite
rules are reduced to lemmas about Z, most of which are inconsistent (and
therefore indicate rewrite rules which are missing side-conditions).

One bad rewrite rule was found in this process, and corrected in
0842563b23f8d780f4ff1080d7620fc3f368191f

The next step after this will be using the rewrite rule correctness to
prove the rewriter correct.

4 files changed, 728 insertions, 22 deletions

diff --git a/_CoqProject b/_CoqProject
index 70fca8fd2..0b4816189 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -264,6 +264,7 @@ src/Experiments/NewPipeline/MiscCompilerPassesProofs.v
 src/Experiments/NewPipeline/Rewriter.v
 src/Experiments/NewPipeline/RewriterProofs.v
 src/Experiments/NewPipeline/RewriterRulesGood.v
+src/Experiments/NewPipeline/RewriterRulesInterpGood.v
 src/Experiments/NewPipeline/RewriterWf1.v
 src/Experiments/NewPipeline/RewriterWf2.v
 src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
new file mode 100644
index 000000000..7647b1f06
--- /dev/null
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -0,0 +1,532 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.MSets.MSetPositive.
+Require Import Coq.FSets.FMapPositive.
+Require Import Crypto.Experiments.NewPipeline.Language.
+Require Import Crypto.Experiments.NewPipeline.LanguageInversion.
+Require Import Crypto.Experiments.NewPipeline.LanguageWf.
+Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs.
+Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypesProofs.
+Require Import Crypto.Experiments.NewPipeline.Rewriter.
+Require Import Crypto.Experiments.NewPipeline.RewriterWf1.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+Require Import Crypto.Util.ZUtil.Hints.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.ZSimplify.Core.
+Require Import Crypto.Util.ZUtil.ZSimplify.
+Require Import Crypto.Util.ZUtil.ZSimplify.Simple.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.AddGetCarry.
+Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Zselect.
+Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.SpecializeAllWays.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.ForallIn.
+Require Import Crypto.Util.NatUtil.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.CPSNotations.
+Require Import Crypto.Util.HProp.
+Require Import Crypto.Util.Decidable.
+Import ListNotations. Local Open Scope list_scope.
+Local Open Scope Z_scope.
+
+Import EqNotations.
+Module Compilers.
+  Import Language.Compilers.
+  Import LanguageInversion.Compilers.
+  Import LanguageWf.Compilers.
+  Import UnderLetsProofs.Compilers.
+  Import GENERATEDIdentifiersWithoutTypesProofs.Compilers.
+  Import Rewriter.Compilers.
+  Import RewriterWf1.Compilers.
+  Import expr.Notations.
+  Import RewriterWf1.Compilers.RewriteRules.
+  Import defaults.
+
+  Module Import RewriteRules.
+    Import Rewriter.Compilers.RewriteRules.
+
+    Local Lemma rlist_rect_eq {var A P ivar} Pnil Pcons ls
+      : @rlist_rect var A P ivar Pnil Pcons ls
+        = match invert_expr.reflect_list ls with
+          | Some ls
+            => Some (list_rect
+                       (fun _ => _)
+                       Pnil
+                       (fun x xs rec => rec' <-- rec; Pcons x xs rec')
+                       ls)%under_lets
+          | None => None
+          end.
+    Proof. cbv [rlist_rect Compile.option_bind' Option.bind]; reflexivity. Qed.
+
+    Local Lemma UnderLets_interp_list_rect {A P} Pnil Pcons ls
+      : UnderLets.interp
+          (@ident.interp)
+          (list_rect
+             (fun _ : list A => UnderLets.UnderLets base.type ident _ P)
+             Pnil
+             (fun x xs rec => rec' <-- rec; Pcons x xs rec')
+             ls)%under_lets
+        = list_rect
+            (fun _ => P)
+            (UnderLets.interp (@ident.interp) Pnil)
+            (fun x xs rec => UnderLets.interp (@ident.interp) (Pcons x xs rec))
+            ls.
+    Proof.
+      induction ls as [|x xs IHxs]; cbn [list_rect]; [ reflexivity | ].
+      rewrite UnderLets.interp_splice, IHxs; reflexivity.
+    Qed.
+
+    Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) (@pattern.ident.to_typed) (@ident.interp)).
+
+    Local Ltac do_cbv0 :=
+      cbv [id
+             Compile.rewrite_rules_interp_goodT
+             Compile.rewrite_rule_data_interp_goodT Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT' Compile.pattern_default_interp pattern.type.under_forall_vars_relation Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.forall2_type_of_list_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule_cps_id_hypsT Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related Compile.value'_interp_related].
+    Local Ltac do_cbv :=
+      do_cbv0;
+      cbv [List.map List.fold_right List.rev list_rect orb List.app].
+
+    Local Ltac start_interp_good :=
+      do_cbv;
+      lazymatch goal with
+      | [ |- forall x p, In (@existT ?A ?P x p) ?ls -> @?Q x p ]
+        => let Q' := fresh in
+           pose Q as Q';
+           change (forall x p, In (@existT A P x p) ls -> Q' x p);
+           apply (@forall_In_existT A P Q' ls); cbn [projT1 projT2]; cbv [id];
+           subst Q'; cbn [projT1 projT2]
+      end;
+      do_cbv0;
+      repeat first [ progress intros
+                   | match goal with
+                     | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl)
+                     | [ |- True /\ _ ] => split; [ exact I | ]
+                     end
+                   | progress cbn [eq_rect] in * ];
+      cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.interp ident.gen_interp] in *.
+
+    Local Ltac interp_good_t_step :=
+      first [ reflexivity
+            | match goal with
+              | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
+              | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand
+              end
+            | progress cbn [expr.interp ident.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr] in *
+            | progress cbv [Compile.option_bind' respectful] in *
+            | progress fold (@type.interp _ base.interp)
+            | progress fold (@base.interp)
+            | match goal with
+              | [ |- context[List.map _ (Lists.List.repeat _ _)] ] => rewrite map_repeat
+              | [ |- context[List.map _ (List.map _ _)] ] => rewrite map_map
+              | [ |- context[List.map (fun x => x) _] ] => rewrite map_id
+              | [ |- context[List.map _ (List.rev _)] ] => rewrite map_rev
+              | [ |- context[List.map _ (firstn _ _)] ] => rewrite <- firstn_map
+              | [ |- context[List.map _ (skipn _ _)] ] => rewrite <- skipn_map
+              | [ |- context[List.length (List.map _ _)] ] => rewrite map_length
+              | [ |- context[List.combine (List.map _ _) _] ] => rewrite combine_map_l
+              | [ |- context[List.combine _ (List.map _ _)] ] => rewrite combine_map_r
+              | [ |- context[expr.interp _ (reify_list _)] ] => rewrite interp_reify_list
+              | [ |- context[expr.interp _ (UnderLets.to_expr ?e)] ] => rewrite UnderLets.interp_to_expr
+              | [ |- context[UnderLets.interp _ (UnderLets.splice_list _ _)] ] => rewrite UnderLets.interp_splice_list
+              | [ |- context[rlist_rect] ] => rewrite rlist_rect_eq
+              | [ |- context[UnderLets.interp _ (list_rect _ _ _ _)] ] => rewrite UnderLets_interp_list_rect
+              | [ |- context[UnderLets.interp _ (UnderLets.splice _ _)] ] => rewrite UnderLets.interp_splice
+              | [ |- context[list_rect _ _ _ (List.map _ _)] ] => rewrite list_rect_map
+              | [ |- list_rect _ _ _ _ = List.app ?ls1 ?ls2 ]
+                =>  rewrite (eq_app_list_rect ls1 ls2)
+              | [ |- list_rect _ _ _ _ = @flat_map ?A ?B ?f ?ls ]
+                =>  rewrite (@eq_flat_map_list_rect A B f ls)
+              | [ |- list_rect _ _ _ _ = @partition ?A ?f ?ls ]
+                =>  rewrite (@eq_partition_list_rect A f ls)
+              | [ |- list_rect _ _ _ _ = @List.map ?A ?B ?f ?ls ]
+                => rewrite (@eq_map_list_rect A B f ls)
+              | [ |- _ = @fold_right ?A ?B ?f ?v ?ls ]
+                =>  rewrite (@eq_fold_right_list_rect A B f v ls)
+              end
+            | progress intros
+            | progress subst
+            | progress inversion_option
+            | progress Z.ltb_to_lt
+            | progress split_andb
+            | match goal with
+              | [ |- Lists.List.repeat _ _ = Lists.List.repeat _ _ ] => apply f_equal2
+              | [ |- firstn _ _ = firstn _ _ ] => apply f_equal2
+              | [ |- skipn _ _ = skipn _ _ ] => apply f_equal2
+              | [ |- rev _ = rev _ ] => apply f_equal
+              | [ |- List.app ?l1 ?l2 = List.app ?l1' ?l2 ] => apply f_equal2
+              | [ |- List.app ?l1 ?l2 = List.app ?l1 ?l2' ] => apply f_equal2
+              | [ |- cons _ _ = cons _ _ ] => apply f_equal2
+              | [ |- list_rect _ ?Pnil ?Pcons ?ls = list_rect _ ?Pnil ?Pcons' ?ls ]
+                => apply list_rect_Proper; [ reflexivity | repeat intro | reflexivity ]
+              | [ |- bool_rect _ ?x ?y ?b = bool_rect _ ?x ?y ?b' ]
+                => apply f_equal3; [ reflexivity | reflexivity | solve [ repeat interp_good_t_step ] ]
+              | [ H : expr.wf _ ?v1 ?v2 |- expr.interp _ ?v1 = expr.interp _ ?v2 ]
+                => apply (expr.wf_interp_Proper _ _ _ H ltac:(assumption))
+              | [ |- ?R (?f (?g (if ?b then ?x else ?y))) (bool_rect ?A ?B ?C ?D) ]
+                => rewrite <- (@Bool.pull_bool_if _ _ g b), <- (@Bool.pull_bool_if _ _ f b);
+                   change (R (bool_rect _ (f (g x)) (f (g y)) b) (bool_rect A B C D))
+              | [ |- context[invert_expr.reflect_list ?ls] ]
+                => destruct (invert_expr.reflect_list ls) eqn:?; expr.invert_subst
+              | [ |- ?f (nth_default _ _ _) = _ ]
+                => rewrite <- (@map_nth_default_always _ _ f)
+              | [ |- map ?f ?ls = map ?g ?ls ] => apply map_ext_in
+              | [ |- List.map _ (update_nth _ _ _) = update_nth _ _ _ ] => apply map_update_nth_ext
+              | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
+              | [ H : forall v : unit, _ |- _ ] => specialize (H tt)
+              | [ H : _ = expr.interp ?ii ?v |- _ ] => is_var v; generalize dependent (expr.interp ii v); clear v
+              | [ |- bool_rect _ _ _ ?b = bool_rect _ _ _ ?b ]
+                => is_var b; destruct b; cbv [bool_rect]
+              | [ H : (forall x y, _ -> expr.interp _ (UnderLets.interp _ (?f1 x)) = expr.interp _ (UnderLets.interp _ (?f2 y)))
+                  |- expr.interp _ (UnderLets.interp _ (?f1 ?x1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2)) ]
+                => apply H
+              | [ H : (forall x y, _ -> forall x' y', _ -> expr.interp _ (UnderLets.interp _ (?f1 x x')) = expr.interp _ (UnderLets.interp _ (?f2 y y')))
+                  |- expr.interp _ (UnderLets.interp _ (?f1 ?x1 ?y1)) = expr.interp _ (UnderLets.interp _ (?f2 ?x2 ?y2)) ]
+                => apply H
+              | [ |- context G[rwhen ?v ?b] ]
+                => let c := constr:(rwhen v b) in
+                   let c := (eval cbv [rwhen] in c) in
+                   let G' := context G[c] in
+                   change G';
+                   destruct b eqn:?
+              | [ |- context G[rwhenl ?v ?b] ]
+                => let c := constr:(rwhenl v b) in
+                   let c := (eval cbv [rwhenl] in c) in
+                   let G' := context G[c] in
+                   change G';
+                   destruct b eqn:?
+              | [ H : negb ?b = true |- _ ] => rewrite (@Bool.negb_true_iff b) in H
+              | [ |- context[expr.interp ?ii ?v] ]
+                => is_var v; generalize dependent (expr.interp ii v); clear v; intro v
+              | [ |- context[Z.mul_split ?a ?b ?c] ]
+                => rewrite (surjective_pairing (Z.mul_split a b c)), Z.mul_split_div, Z.mul_split_mod
+              | [ |- context[Z.zselect] ] => rewrite Z.zselect_correct
+              | [ |- context[Z.sub_get_borrow_full ?a ?b ?c] ]
+                => rewrite (surjective_pairing (Z.sub_get_borrow_full a b c)), Z.sub_get_borrow_full_div, Z.sub_get_borrow_full_mod
+              | [ |- context[Z.sub_with_get_borrow_full ?a ?b ?c ?d] ]
+                => rewrite (surjective_pairing (Z.sub_with_get_borrow_full a b c d)), Z.sub_with_get_borrow_full_div, Z.sub_with_get_borrow_full_mod
+              | [ |- context[Z.add_get_carry_full ?a ?b ?c] ]
+                => rewrite (surjective_pairing (Z.add_get_carry_full a b c)), Z.add_get_carry_full_div, Z.add_get_carry_full_mod
+              | [ |- context[Z.add_with_get_carry_full ?a ?b ?c ?d] ]
+                => rewrite (surjective_pairing (Z.add_with_get_carry_full a b c d)), Z.add_with_get_carry_full_div, Z.add_with_get_carry_full_mod
+              | [ |- pair _ _ = pair _ _ ] => apply f_equal2
+              | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia
+              | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia
+              | [ |- Z.opp _ = Z.opp _ ] => apply f_equal
+              end
+            | match goal with
+              | [ |- context[?f (list_rect _ _ _ _)] ]
+                => match f with
+                   | expr.interp _ => idtac
+                   | Compile.reify_expr => idtac
+                   end;
+                   erewrite (@push_f_list_rect _ _ f)
+                     by (intros;
+                         repeat first [ progress cbn [expr.interp ident.interp ident.gen_interp UnderLets.interp Compile.reify_expr]
+                                      | rewrite UnderLets.interp_splice ];
+                         match goal with
+                         | [ |- ?LHS = ?Pcons' ?x ?xs ?rec ]
+                           => let LHS' := match (eval pattern x, xs, rec in LHS) with ?f _ _ _ => f end in
+                              unify Pcons' LHS'; reflexivity
+                         end)
+              | [ |- context[?f (nat_rect _ _ _ _)] ]
+                => match f with
+                   | expr.interp _ => idtac
+                   | UnderLets.interp _ => idtac
+                   | Compile.reify_expr => idtac
+                   end;
+                   erewrite (@push_f_nat_rect _ _ f)
+                     by (intros;
+                         repeat first [ progress cbn [expr.interp ident.interp ident.gen_interp UnderLets.interp Compile.reify_expr]
+                                      | rewrite UnderLets.interp_splice ];
+                         match goal with
+                         | [ |- ?LHS = ?PS' ?x ?rec ]
+                           => let LHS' := match (eval pattern x, rec in LHS) with ?f _ _ => f end in
+                              unify PS' LHS'; reflexivity
+                         end)
+              | [ |- ?f (list_rect _ _ _ _) = list_rect _ _ _ _ ]
+                => match f with
+                   | expr.interp _ => idtac
+                   | Compile.reify_expr => idtac
+                   end;
+                   erewrite (@push_f_list_rect _ _ f);
+                   [ apply list_rect_Proper; repeat intro; try reflexivity | ]
+              | [ |- ?f (nat_rect _ _ _ _) = nat_rect _ _ _ _ ]
+                => match f with
+                   | expr.interp _ => idtac
+                   | UnderLets.interp _ => idtac
+                   | Compile.reify_expr => idtac
+                   end;
+                   erewrite (@push_f_nat_rect _ _ f);
+                   [ apply nat_rect_Proper_nondep; repeat intro; try reflexivity | ]
+              end
+            | break_innermost_match_step
+            | break_innermost_match_hyps_step
+            | match goal with
+              | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))]
+                  |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ]
+                => apply H
+              | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith
+              | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith
+              | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r
+              | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H
+              | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ]
+                => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith
+              | [ |- _ = _ :> BinInt.Z ] => progress normalize_commutative_identifier Z.land Z.land_comm
+              | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => exfalso; apply H', H
+              | [ H : ?x = 2^Z.log2_up ?x - 1 |- context[2^Z.log2_up ?x - 1] ] => rewrite <- H
+              | [ H : ?x = 2^Z.log2 ?x, H' : context[2^Z.log2 ?x] |- _ = _ :> BinInt.Z ]
+                => rewrite <- H in H'
+              | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const
+              | [ |- ?f (?g (nat_rect _ _ _ ?n ?v)) = nat_rect _ _ _ ?n _ ]
+                => revert v; is_var n; induction n; intro v; cbn [nat_rect]
+              | [ |- _ mod ?x = _ mod ?x ]
+                => progress (push_Zmod; pull_Zmod)
+              | [ |- _ mod ?x = _ mod ?x ]
+                => apply f_equal2; (lia + nia)
+              | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast
+              end ].
+
+    Lemma nbe_rewrite_rules_interp_good
+      : rewrite_rules_interp_goodT nbe_rewrite_rules.
+    Proof using Type.
+      Time start_interp_good.
+      Time all: repeat interp_good_t_step.
+    Qed.
+
+    Axiom proof_admitted : False.
+    Local Notation admit := (match proof_admitted with end).
+
+    Lemma arith_rewrite_rules_interp_good max_const
+      : rewrite_rules_interp_goodT (arith_rewrite_rules max_const).
+    Proof using Type.
+      Time start_interp_good.
+      Time all: try solve [ repeat interp_good_t_step; (lia + nia) ].
+      (* This is mainly for display *)
+      all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
+                        | progress subst
+                        | match goal with
+                          | [ H : context[expr.interp ?ii ?v] |- _ ]
+                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                          | [ |- context[expr.interp ?ii ?v] ]
+                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                          end ].
+      (* 9 subgoals (ID 30397)
+
+  max_const, x, x0 : Z
+  v1 : expr (type.base base.type.Z)
+  ============================
+  match
+    (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1);
+     Some (UnderLets.Base x1))%option
+  with
+  | Some v0 =>
+      expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
+      Z.mul_split x x0 (expr.interp (@ident.interp) v1)
+  | None => True
+  end
+
+subgoal 2 (ID 30445) is:
+ match
+   (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1);
+    Some (UnderLets.Base x1))%option
+ with
+ | Some v0 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
+     Z.mul_split x (expr.interp (@ident.interp) v1) x0
+ | None => True
+ end
+subgoal 3 (ID 30493) is:
+ match
+   (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1);
+    Some (UnderLets.Base x1))%option
+ with
+ | Some v0 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
+     Z.mul_split x x0 (expr.interp (@ident.interp) v1)
+ | None => True
+ end
+subgoal 4 (ID 30541) is:
+ match
+   (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1);
+    Some (UnderLets.Base x1))%option
+ with
+ | Some v0 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
+     Z.mul_split x (expr.interp (@ident.interp) v1) x0
+ | None => True
+ end
+subgoal 5 (ID 30631) is:
+ match
+   (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0);
+    Some (UnderLets.Base x0))%option
+ with
+ | Some v1 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v1) =
+     Z.add_get_carry_full v2 x (expr.interp (@ident.interp) v0)
+ | None => True
+ end
+subgoal 6 (ID 30721) is:
+ match
+   (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0);
+    Some (UnderLets.Base x0))%option
+ with
+ | Some v1 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v1) =
+     Z.add_get_carry_full v2 (expr.interp (@ident.interp) v0) x
+ | None => True
+ end
+subgoal 7 (ID 30772) is:
+ match
+   (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0));
+    Some (UnderLets.Base x2))%option
+ with
+ | Some v0 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
+     Z.add_with_get_carry_full x x0 x1 (expr.interp (@ident.interp) v1)
+ | None => True
+ end
+subgoal 8 (ID 30824) is:
+ match
+   (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0));
+    Some (UnderLets.Base x2))%option
+ with
+ | Some v0 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v0) =
+     Z.add_with_get_carry_full x x0 (expr.interp (@ident.interp) v1) x1
+ | None => True
+ end
+subgoal 9 (ID 30915) is:
+ match
+   rwhenl
+     (Some
+        (UnderLets.UnderLet
+           (#(ident.Z_add_with_get_carry)%expr @ v1 @ v0 @ (##x)%expr @
+            (##x0)%expr)%expr_pat
+           (fun vc : Z * Z =>
+            UnderLets.Base (#(ident.fst)%expr @ ($vc)%expr, (##0)%expr)%expr_pat)))
+     ((x =? 0) && (x0 =? 0))
+ with
+ | Some v2 =>
+     expr.interp (@ident.interp) (UnderLets.interp (@ident.interp) v2) =
+     Z.add_with_get_carry_full (expr.interp (@ident.interp) v1)
+       (expr.interp (@ident.interp) v0) x x0
+ | None => True
+ end
+*)
+      1-9: exact admit.
+    Qed.
+
+    Local Ltac fancy_local_t :=
+      repeat first [ match goal with
+                     | [ H : forall s v v', ?invert_low s v = Some v' -> v = _,
+                           H' : ?invert_low _ _ = Some _ |- _ ] => apply H in H'
+                     end
+                   | progress autorewrite with zsimplify in * ].
+
+    Lemma fancy_rewrite_rules_interp_good
+            (invert_low invert_high : Z -> Z -> option Z)
+            (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
+            (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
+      : rewrite_rules_interp_goodT (fancy_rewrite_rules invert_low invert_high).
+    Proof using Type.
+      Time start_interp_good.
+      Time all: try solve [
+                      repeat interp_good_t_step;
+                        cbv [Option.bind] in *;
+                        repeat interp_good_t_step;
+                        fancy_local_t;
+                        repeat interp_good_t_step ].
+      Time all: repeat interp_good_t_step.
+      Time all: cbv [Option.bind] in *.
+      Time all: repeat interp_good_t_step.
+      Time all: fancy_local_t.
+      Time all: repeat interp_good_t_step.
+      all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
+                        | progress subst
+                        | match goal with
+                          | [ H : context[expr.interp ?ii ?v] |- _ ]
+                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                          | [ |- context[expr.interp ?ii ?v] ]
+                            => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                          end ].
+      all: repeat match goal with
+                  | [ H : _ = _ :> BinInt.Z |- _ ] => revert H
+                  | [ v : BinInt.Z |- _ ] => clear v || revert v
+                  end.
+      (* 16 subgoals (ID 100240)
+
+  invert_low, invert_high : Z -> Z -> option Z
+  Hlow : forall s v v' : Z,
+         invert_low s v = Some v' -> v = Z.land v' (2 ^ (s / 2) - 1)
+  Hhigh : forall s v v' : Z, invert_high s v = Some v' -> v = Z.shiftr v' (s / 2)
+  ============================
+  forall x x0 v1 v0 : Z,
+  x = 2 ^ Z.log2 x -> (v1 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0) / x
+
+subgoal 2 (ID 100250) is:
+ forall x x0 v0 v1 : Z,
+ x = 2 ^ Z.log2 x -> (v0 + Z.shiftl v1 x0 mod x) / x = (Z.shiftl v1 x0 + v0) / x
+subgoal 3 (ID 100260) is:
+ forall x x0 v1 v0 : Z,
+ x = 2 ^ Z.log2 x -> (v1 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0) / x
+subgoal 4 (ID 100270) is:
+ forall x x0 v0 v1 : Z,
+ x = 2 ^ Z.log2 x -> (v0 + Z.shiftr v1 x0 mod x) / x = (Z.shiftr v1 x0 + v0) / x
+subgoal 5 (ID 100278) is:
+ forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 + v0 mod x) / x = (v1 + v0) / x
+subgoal 6 (ID 100290) is:
+ forall x x0 v1 v0 v4 : Z,
+ x = 2 ^ Z.log2 x ->
+ (v1 + v0 + Z.shiftl v4 x0 mod x) / x = (v1 + v0 + Z.shiftl v4 x0) / x
+subgoal 7 (ID 100302) is:
+ forall x x0 v1 v4 v0 : Z,
+ x = 2 ^ Z.log2 x ->
+ (v1 + v4 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0 + v4) / x
+subgoal 8 (ID 100314) is:
+ forall x x0 v1 v0 v4 : Z,
+ x = 2 ^ Z.log2 x ->
+ (v1 + v0 + Z.shiftr v4 x0 mod x) / x = (v1 + v0 + Z.shiftr v4 x0) / x
+subgoal 9 (ID 100326) is:
+ forall x x0 v1 v4 v0 : Z,
+ x = 2 ^ Z.log2 x ->
+ (v1 + v4 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0 + v4) / x
+subgoal 10 (ID 100336) is:
+ forall x v1 v0 v4 : Z,
+ x = 2 ^ Z.log2 x -> (v1 + v0 + v4 mod x) / x = (v1 + v0 + v4) / x
+subgoal 11 (ID 100346) is:
+ forall x x0 v1 v0 : Z,
+ x = 2 ^ Z.log2 x -> (v1 - Z.shiftl v0 x0 mod x) / x = (v1 - Z.shiftl v0 x0) / x
+subgoal 12 (ID 100356) is:
+ forall x x0 v1 v0 : Z,
+ x = 2 ^ Z.log2 x -> (v1 - Z.shiftr v0 x0 mod x) / x = (v1 - Z.shiftr v0 x0) / x
+subgoal 13 (ID 100364) is:
+ forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 - v0 mod x) / x = (v1 - v0) / x
+subgoal 14 (ID 100376) is:
+ forall x x0 v1 v0 v4 : Z,
+ x = 2 ^ Z.log2 x ->
+ (v0 - Z.shiftl v4 x0 mod x - v1) / x = (v0 - Z.shiftl v4 x0 - v1) / x
+subgoal 15 (ID 100388) is:
+ forall x x0 v1 v0 v4 : Z,
+ x = 2 ^ Z.log2 x ->
+ (v0 - Z.shiftr v4 x0 mod x - v1) / x = (v0 - Z.shiftr v4 x0 - v1) / x
+subgoal 16 (ID 100398) is:
+ forall x v1 v0 v4 : Z,
+ x = 2 ^ Z.log2 x -> (v0 - v4 mod x - v1) / x = (v0 - v4 - v1) / x
+*)
+      all: exact admit.
+    Qed.
+  End RewriteRules.
+End Compilers.
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 37e192f07..4f2017cbf 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -204,6 +204,9 @@ Module Compilers.
 
                 (full_types : raw_pident -> Type)
                 (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc))
+                (pident_to_typed
+                 : forall t (idc : pident t) (evm : EvarMap),
+                    type_of_list (pident_arg_types t idc) -> ident (pattern.type.subst_default t evm))
                 (type_of_raw_pident : forall (pidc : raw_pident), full_types pidc -> type.type base.type)
                 (raw_pident_to_typed : forall (pidc : raw_pident) (args : full_types pidc), ident (type_of_raw_pident pidc args))
                 (raw_pident_is_simple : raw_pident -> bool)
@@ -236,15 +239,24 @@ Module Compilers.
         Local Notation to_raw_pattern := (@pattern.to_raw pident raw_pident (@strip_types)).
         Local Notation reify := (@reify ident).
         Local Notation reflect := (@reflect ident).
+        Local Notation reify_expr := (@reify_expr ident).
         Local Notation rawexpr := (@rawexpr ident).
         Local Notation eval_decision_tree var := (@eval_decision_tree ident var pident full_types invert_bind_args type_of_raw_pident raw_pident_to_typed).
         Local Notation reveal_rawexpr e := (@reveal_rawexpr_cps ident _ e _ id).
         Local Notation unify_pattern' var := (@unify_pattern' ident var pident pident_arg_types pident_unify pident_unify_unknown).
         Local Notation unify_pattern var := (@unify_pattern ident var pident pident_arg_types pident_unify pident_unify_unknown type_vars_of_pident).
 
+        Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls
+          := list_rect
+               (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls)
+               (fun f => f tt)
+               (fun T Ts rec k t => rec (fun ts => k (t, ts)))
+               ls.
+
         Section with_var1.
           Context {var : type -> Type}.
           Local Notation expr := (@expr.expr base.type ident var).
+          Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var).
 
           Local Notation "e1 === e2" := (existT expr _ e1 = existT expr _ e2) : type_scope.
 
@@ -572,27 +584,37 @@ Module Compilers.
                          | break_match_step ltac:(fun _ => idtac) ].
           Qed.
 
-          Lemma normalize_deep_rewrite_rule_cps_id
-                {should_do_again with_opt under_lets is_cps t v T k}
-                (Hk : k None = None)
-                (Hv : (match is_cps, with_opt return @deep_rewrite_ruleTP_gen ident var should_do_again with_opt under_lets is_cps t -> Prop
-                       with
-                       | true, true => fun v => forall T k, v T k = k (v _ id)
-                       | true, false => fun v => forall T k, v T k = (v' <- v _ (@Some _); k v')%option
-                       | false, _ => fun _ => True
-                       end)
-                        v)
-            : @normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v T k = k (@normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v _ id).
-          Proof using Type.
-            clear -Hv Hk; cbn in *.
-            repeat first [ progress cbn in *
-                         | progress destruct_head'_bool
-                         | reflexivity
-                         | progress cbv [id Option.bind] in *
-                         | solve [ auto ]
-                         | break_innermost_match_step
-                         | rewrite Hv; (solve [ auto ] + break_innermost_match_step) ].
-          Qed.
+          Section normalize_deep_rewrite_rule_cps_id.
+            Context {should_do_again with_opt under_lets is_cps : bool}
+                    {t}
+                    {v : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t}
+                    {T}
+                    {k : option (UnderLets var (@expr.expr base.type ident (if should_do_again then @value var else var) t)) -> option T}.
+
+            Definition normalize_deep_rewrite_rule_cps_id_hypsT
+              := ((match is_cps, with_opt return @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t -> Prop
+                   with
+                   | true, true => fun v => forall T k, v T k = k (v _ id)
+                   | true, false => fun v => forall T k, v T k = (v' <- v _ (@Some _); k v')%option
+                   | false, _ => fun _ => True
+                   end)
+                    v).
+
+            Lemma normalize_deep_rewrite_rule_cps_id
+                  (Hk : k None = None)
+                  (Hv : normalize_deep_rewrite_rule_cps_id_hypsT)
+              : @normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v T k = k (@normalize_deep_rewrite_rule ident var should_do_again with_opt under_lets is_cps t v _ id).
+            Proof using Type.
+              clear -Hk Hv; cbv [normalize_deep_rewrite_rule_cps_id_hypsT] in *; cbn in *.
+              repeat first [ progress cbn in *
+                           | progress destruct_head'_bool
+                           | reflexivity
+                           | progress cbv [id Option.bind] in *
+                           | solve [ auto ]
+                           | break_innermost_match_step
+                           | rewrite Hv; (solve [ auto ] + break_innermost_match_step) ].
+            Qed.
+          End normalize_deep_rewrite_rule_cps_id.
         End with_var1.
 
         Section with_var2.
@@ -671,6 +693,26 @@ Module Compilers.
               eapply wf_reify; auto. }
           Qed.
 
+          Lemma wf_reify_expr G G' {t}
+                (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @wf_value G' t v1 v2)
+                e1 e2
+                (Hwf : expr.wf G e1 e2)
+            : expr.wf G' (@reify_expr var1 t e1) (@reify_expr var2 t e2).
+          Proof using Type.
+            cbv [wf_value] in *; revert dependent G'; induction Hwf; intros; cbn [reify_expr];
+              first [ constructor | apply wf_reify ]; eauto; intros.
+            all: match goal with H : _ |- _ => apply H end.
+            all: repeat first [ progress cbn [In eq_rect] in *
+                              | progress intros
+                              | progress destruct_head'_or
+                              | progress subst
+                              | progress inversion_sigma
+                              | progress inversion_prod
+                              | apply wf_reflect
+                              | solve [ eapply wf_value'_Proper_list; [ | solve [ eauto ] ]; wf_safe_t ]
+                              | constructor ].
+          Qed.
+
           Inductive wf_rawexpr : list { t : type & var1 t * var2 t }%type -> forall {t}, @rawexpr var1 -> @expr var1 t -> @rawexpr var2 -> @expr var2 t -> Prop :=
           | Wf_rIdent {t} G known (idc : ident t) : wf_rawexpr G (rIdent known idc (expr.Ident idc)) (expr.Ident idc) (rIdent known idc (expr.Ident idc)) (expr.Ident idc)
           | Wf_rApp {s d} G
@@ -994,6 +1036,137 @@ Module Compilers.
                                (rew [fun tp => @rewrite_rule_data1 _ (pattern.pattern_of_anypattern tp)] pf in r1)
                                r2 }).
         End with_var2.
+
+        Section with_interp.
+          Context (ident_interp : forall t, ident t -> type.interp base.interp t)
+                  {ident_interp_Proper : forall t, Proper (eq ==> type.eqv) (ident_interp t)}.
+          Local Notation var := (type.interp base.interp) (only parsing).
+          Local Notation expr := (@expr.expr base.type ident var).
+          Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation with_unif_rewrite_ruleTP_gen := (@with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation with_unification_resultT' := (@with_unification_resultT' ident var pident pident_arg_types).
+          Local Notation normalize_deep_rewrite_rule := (@normalize_deep_rewrite_rule ident var).
+          Local Notation under_with_unification_resultT_relation := (@under_with_unification_resultT_relation ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation under_with_unification_resultT_relation_hetero := (@under_with_unification_resultT_relation_hetero ident var pident pident_arg_types type_vars_of_pident).
+          Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var).
+
+          Local Notation UnderLets_maybe_interp with_lets
+            := (if with_lets as with_lets' return (if with_lets' then UnderLets var _ else _) -> _
+                then UnderLets.interp ident_interp
+                else (fun x => x)).
+
+          Fixpoint value'_interp_related
+                   {with_lets1 with_lets2 t}
+            : @value' var with_lets1 t
+              -> @value' var with_lets2 t
+              -> Prop
+            := match t return value' _ t -> value' _ t -> Prop with
+               | type.base t
+                 => fun v1 v2
+                    => expr.interp ident_interp (UnderLets_maybe_interp with_lets1 v1)
+                       == expr.interp ident_interp (UnderLets_maybe_interp with_lets2 v2)
+               | type.arrow s d
+                 => fun (f1 f2 : value' _ s -> value' _ d)
+                    => forall x1 x2,
+                        @value'_interp_related _ _ s x1 x2
+                        -> @value'_interp_related _ _ d (f1 x1) (f2 x2)
+               end.
+
+          Definition value_interp_related {t} : relation (@value var t)
+            := value'_interp_related.
+
+          Lemma interp_reify_reflect {with_lets t} e v
+            : expr.interp ident_interp e == v -> expr.interp ident_interp (@reify _ with_lets t (reflect e)) == v.
+          Proof using Type.
+            revert with_lets; induction t as [|s IHs d IHd]; intro;
+              cbn [type.related reflect reify];
+              fold (@reify var) (@reflect var); cbv [respectful]; break_innermost_match;
+                cbn [expr.interp UnderLets.to_expr]; auto; [].
+            intros Hf ? ? Hx.
+            apply IHd; cbn [expr.interp]; auto.
+          Qed.
+
+          Lemma interp_of_wf_reify_expr G {t}
+                (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp ident_interp (reify v1) == v2)
+                e1 e2
+                (Hwf : expr.wf G e1 e2)
+            : expr.interp ident_interp (@reify_expr _ t e1) == expr.interp ident_interp e2.
+          Proof using ident_interp_Proper.
+            induction Hwf; cbn [expr.interp reify_expr]; cbv [LetIn.Let_In];
+              try solve [ auto
+                        | apply ident_interp_Proper; reflexivity ].
+            all: cbn [type.related] in *; cbv [respectful]; intros.
+            all: match goal with H : _ |- _ => apply H; clear H end.
+            all: repeat first [ progress cbn [In eq_rect fst snd] in *
+                              | progress intros
+                              | progress destruct_head'_or
+                              | progress subst
+                              | progress inversion_sigma
+                              | progress inversion_prod
+                              | apply interp_reify_reflect
+                              | solve [ auto ] ].
+          Qed.
+
+          Fixpoint pattern_default_interp' {K t} (p : pattern t) evm {struct p} : (expr (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' t p evm K
+            := match p in pattern.pattern t return (expr (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' t p evm K with
+               | pattern.Wildcard t => fun k v => k (reify v)
+               | pattern.Ident t idc
+                 => fun k
+                    => lam_type_of_list (fun args => k (expr.Ident (pident_to_typed _ idc _ args)))
+               | pattern.App s d f x
+                 => fun k
+                    => @pattern_default_interp'
+                         _ _ f evm
+                         (fun ef
+                          => @pattern_default_interp'
+                               _ _ x evm
+                               (fun ex
+                                => k (expr.App ef ex)))
+               end.
+
+          Definition pattern_default_interp {t} (p : pattern t) : @with_unif_rewrite_ruleTP_gen t p false false false false
+            := pattern.type.lam_forall_vars
+                 (fun evm
+                  => pattern_default_interp' p evm id).
+
+          Definition deep_rewrite_ruleTP_gen_good_relation
+                     {should_do_again with_opt under_lets is_cps : bool} {t}
+                     (v1 : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets is_cps t)
+                     (v2 : expr t)
+            : Prop
+            := @normalize_deep_rewrite_rule_cps_id_hypsT var _ _ _ _ _ v1
+               /\ (let v1 := normalize_deep_rewrite_rule v1 _ id in
+                   match v1 with
+                   | None => True
+                   | Some v1 => let v1 := UnderLets.interp ident_interp v1 in
+                                (if should_do_again
+                                    return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> Prop
+                                 then
+                                   (fun v1
+                                    => expr.interp ident_interp (reify_expr v1) == expr.interp ident_interp v2)
+                                 else
+                                   (fun v1 => expr.interp ident_interp v1 == expr.interp ident_interp v2))
+                                  v1
+                   end).
+
+          Definition rewrite_rule_data_interp_goodT
+                     {t} {p : pattern t} (r : @rewrite_rule_data t p)
+            : Prop
+            := @under_with_unification_resultT_relation_hetero
+                 _ _ _ _
+                 (fun _ => value_interp_related)
+                 (fun evm => deep_rewrite_ruleTP_gen_good_relation)
+                 (rew_replacement _ _ r)
+                 (pattern_default_interp p).
+
+          Definition rewrite_rules_interp_goodT
+                     (rews : rewrite_rulesT)
+            : Prop
+            := forall p r,
+              List.In (existT _ p r) rews
+              -> rewrite_rule_data_interp_goodT r.
+        End with_interp.
       End with_var.
     End Compile.
   End RewriteRules.
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index 6b2d92971..de17f2896 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -799,7 +799,7 @@ Module Compilers.
                                        => rewrite ap_transport_Base
                                      | [ |- True ] => exact I
                                      end
-                                   | progress cbv [wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen option_bind'] in *
+                                   | progress cbv [wf_rewrite_rule_data wf_with_unif_rewrite_ruleTP_gen option_bind' normalize_deep_rewrite_rule_cps_id_hypsT] in *
                                    | lazymatch goal with
                                      | [ |- (@unify_pattern1 ?t ?re1 ?p ?K1 ?v1 ?T1 ?cont1 = None
                                              <-> @unify_pattern2 ?t ?re2 ?p ?K2 ?v2 ?T2 ?cont2 = None)