Clean up and improve Reflection.Relations

13 files changed, 310 insertions, 298 deletions

diff --git a/src/Reflection/InterpWfRel.v b/src/Reflection/InterpWfRel.v
index b4cccf9dc..9106ecb5a 100644
--- a/src/Reflection/InterpWfRel.v
+++ b/src/Reflection/InterpWfRel.v
@@ -17,8 +17,8 @@ Section language.
           (interp_op1 : forall src dst, op src dst -> interp_flat_type interp_base_type1 src -> interp_flat_type interp_base_type1 dst)
           (interp_op2 : forall src dst, op src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst)
           {R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop}
-          (Rop : forall src dst op sv1 sv2, interp_flat_type_rel_pointwise2 R sv1 sv2
-                                            -> interp_flat_type_rel_pointwise2
+          (Rop : forall src dst op sv1 sv2, interp_flat_type_rel_pointwise R sv1 sv2
+                                            -> interp_flat_type_rel_pointwise
                                                  R (interp_op1 src dst op sv1) (interp_op2 src dst op sv2)).
 
   Local Notation exprf1 := (@exprf base_type_code op interp_base_type1).
@@ -33,9 +33,9 @@ Section language.
   Local Notation Interp1 := (@Interp base_type_code interp_base_type1 op interp_op1).
   Local Notation Interp2 := (@Interp base_type_code interp_base_type2 op interp_op2).
 
-  Lemma interp_flat_type_rel_pointwise2_flatten_binding_list
+  Lemma interp_flat_type_rel_pointwise_flatten_binding_list
         {t x x' T e1 e2}
-        (Hpointwise : interp_flat_type_rel_pointwise2 R e1 e2)
+        (Hpointwise : interp_flat_type_rel_pointwise R e1 e2)
         (HIn : List.In (existT (fun t : base_type_code => (interp_base_type1 t * interp_base_type2 t)%type) t (x, x')%core)
                        (flatten_binding_list (t:=T) e1 e2))
     : R t x x'.
@@ -50,7 +50,7 @@ Section language.
                    | solve [ eauto ] ].
   Qed.
 
-  Local Hint Resolve List.in_app_or List.in_or_app interp_flat_type_rel_pointwise2_flatten_binding_list.
+  Local Hint Resolve List.in_app_or List.in_or_app interp_flat_type_rel_pointwise_flatten_binding_list.
 
   Section wf.
     Lemma interpf_wff
@@ -60,7 +60,7 @@ Section language.
                  List.In (existT (fun t : base_type_code => (interp_base_type1 t * interp_base_type2 t)%type) t (x, x')%core) G
                  -> R t x x')
              (Rwf : wff G e1 e2)
-    : interp_flat_type_rel_pointwise2 R (interpf1 e1) (interpf2 e2).
+    : interp_flat_type_rel_pointwise R (interpf1 e1) (interpf2 e2).
     Proof.
       induction Rwf; simpl; auto.
       repeat match goal with
diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v
index 35dfd8500..968814d32 100644
--- a/src/Reflection/Relations.v
+++ b/src/Reflection/Relations.v
@@ -6,6 +6,8 @@ Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sigma.
 
+Local Coercion is_true : bool >-> Sortclass.
+
 Local Open Scope ctype_scope.
 Section language.
   Context {base_type_code : Type}.
@@ -13,240 +15,252 @@ Section language.
   Local Notation flat_type := (flat_type base_type_code).
   Local Notation type := (type base_type_code).
 
-  Section type.
-    Context (interp_flat_type : flat_type -> Type)
-            (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop).
-    Local Notation interp_type_gen := (interp_type_gen interp_flat_type).
-    Fixpoint interp_type_gen_rel_pointwise (t : type)
-      : interp_type_gen t -> interp_type_gen t -> Prop :=
-      match t with
-      | Tflat t => R t
-      | Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x)
-      end.
-    Global Instance interp_type_gen_rel_pointwise_Reflexive {H : forall t, Reflexive (R t)}
-      : forall t, Reflexive (interp_type_gen_rel_pointwise t).
-    Proof. induction t; repeat intro; reflexivity. Qed.
-    Global Instance interp_type_gen_rel_pointwise_Symmetric {H : forall t, Symmetric (R t)}
-      : forall t, Symmetric (interp_type_gen_rel_pointwise t).
-    Proof. induction t; simpl; repeat intro; symmetry; eauto. Qed.
-    Global Instance interp_type_gen_rel_pointwise_Transitive {H : forall t, Transitive (R t)}
-      : forall t, Transitive (interp_type_gen_rel_pointwise t).
-    Proof. induction t; simpl; repeat intro; etransitivity; eauto. Qed.
-  End type.
-
-  Section flat_type0.
-    Context {interp_base_type : base_type_code -> Type}
-            (R : forall t, interp_base_type t -> Prop).
-    Local Notation interp_flat_type := (interp_flat_type interp_base_type).
-    Fixpoint interp_flat_type_rel_pointwise0 (t : flat_type)
-      : interp_flat_type t -> Prop :=
-      match t with
-      | Tbase t => R t
-      | Unit => fun _ => True
-      | Prod _ _ => fun x => interp_flat_type_rel_pointwise0 _ (fst x)
-                             /\ interp_flat_type_rel_pointwise0 _ (snd x)
-      end.
-  End flat_type0.
+  Local Ltac rel_relb_t :=
+    repeat first [ progress simpl in *
+                 | reflexivity
+                 | intuition congruence
+                 | setoid_rewrite Bool.andb_true_iff
+                 | intro
+                 | rewrite_hyp <- !* ].
 
   Section flat_type.
-    Context {interp_base_type : base_type_code -> Type}
-            (R : forall t, interp_base_type t -> interp_base_type t -> Prop).
-    Local Notation interp_flat_type := (interp_flat_type interp_base_type).
-    Fixpoint interp_flat_type_rel_pointwise (t : flat_type)
-      : interp_flat_type t -> interp_flat_type t -> Prop :=
-      match t with
-      | Tbase t => R t
-      | Unit => fun _ _ => True
-      | Prod _ _ => fun x y => interp_flat_type_rel_pointwise _ (fst x) (fst y)
-                               /\ interp_flat_type_rel_pointwise _ (snd x) (snd y)
-      end.
-    Definition interp_type_rel_pointwise
-      := interp_type_gen_rel_pointwise _ interp_flat_type_rel_pointwise.
-  End flat_type.
-
-  Section rel_pointwise2.
-    Section type.
-      Section hetero_hetero.
-        Context (interp_src1 interp_src2 : base_type_code -> Type)
-                (interp_dst1 interp_dst2 : flat_type -> Type)
-                (Rsrc : forall t1 t2, interp_src1 t1 -> interp_src2 t2 -> Prop)
-                (Rdst : forall t1 t2, interp_dst1 t1 -> interp_dst2 t2 -> Prop).
+    Context {interp_base_type1 interp_base_type2 : base_type_code -> Type}.
+    Local Notation interp_flat_type1 := (interp_flat_type interp_base_type1).
+    Local Notation interp_flat_type2 := (interp_flat_type interp_base_type2).
 
-        Fixpoint interp_type_gen_rel_pointwise2_hetero_hetero (t1 t2 : type)
-          : interp_type_gen_hetero interp_src1 interp_dst1 t1
-            -> interp_type_gen_hetero interp_src2 interp_dst2 t2
-            -> Prop
+    Section gen_Prop.
+      Context (P : Type)
+              (and : P -> P -> P)
+              (True : P)
+              (False : P).
+      Section pointwise1.
+        Context (R : forall t, interp_base_type1 t -> P).
+        Fixpoint interp_flat_type_rel_pointwise1_gen_Prop (t : flat_type)
+          : interp_flat_type1 t -> P :=
+          match t with
+          | Tbase t => R t
+          | Unit => fun _ => True
+          | Prod _ _ => fun x => and (interp_flat_type_rel_pointwise1_gen_Prop _ (fst x))
+                                     (interp_flat_type_rel_pointwise1_gen_Prop _ (snd x))
+          end.
+      End pointwise1.
+      Section pointwise2.
+        Context (R : forall t, interp_base_type1 t -> interp_base_type2 t -> P).
+        Fixpoint interp_flat_type_rel_pointwise_gen_Prop (t : flat_type)
+          : interp_flat_type1 t -> interp_flat_type2 t -> P :=
+          match t with
+          | Tbase t => R t
+          | Unit => fun _ _ => True
+          | Prod _ _ => fun x y => and (interp_flat_type_rel_pointwise_gen_Prop _ (fst x) (fst y))
+                                       (interp_flat_type_rel_pointwise_gen_Prop _ (snd x) (snd y))
+          end.
+      End pointwise2.
+      Section pointwise2_hetero.
+        Context (R : forall t1 t2, interp_base_type1 t1 -> interp_base_type2 t2 -> P).
+        Fixpoint interp_flat_type_rel_pointwise_hetero_gen_Prop (t1 t2 : flat_type)
+          : interp_flat_type1 t1 -> interp_flat_type2 t2 -> P
           := match t1, t2 with
-             | Tflat t1, Tflat t2 => Rdst t1 t2
-             | Arrow src1 dst1, Arrow src2 dst2
-               => @respectful_hetero _ _ _ _ (Rsrc src1 src2) (fun _ _ => interp_type_gen_rel_pointwise2_hetero_hetero dst1 dst2)
-             | Tflat _, _
-             | Arrow _ _, _
+             | Tbase t1, Tbase t2 => R t1 t2
+             | Unit, Unit => fun _ _ => True
+             | Prod x1 y1, Prod x2 y2
+               => fun a b => and (interp_flat_type_rel_pointwise_hetero_gen_Prop x1 x2 (fst a) (fst b))
+                                 (interp_flat_type_rel_pointwise_hetero_gen_Prop y1 y2 (snd a) (snd b))
+             | Tbase _, _
+             | Unit, _
+             | Prod _ _, _
                => fun _ _ => False
              end.
-        Global Arguments interp_type_gen_rel_pointwise2_hetero_hetero _ _ _ _ / .
-      End hetero_hetero.
+      End pointwise2_hetero.
+    End gen_Prop.
+
+    Definition interp_flat_type_relb_pointwise1
+      := @interp_flat_type_rel_pointwise1_gen_Prop bool andb true.
+    Global Arguments interp_flat_type_relb_pointwise1 _ !_ _ / .
+    Definition interp_flat_type_rel_pointwise1
+      := @interp_flat_type_rel_pointwise1_gen_Prop Prop and True.
+    Global Arguments interp_flat_type_rel_pointwise1 _ !_ _ / .
+    Lemma interp_flat_type_rel_pointwise1_iff_relb {R} t x
+      : interp_flat_type_relb_pointwise1 R t x <-> interp_flat_type_rel_pointwise1 R t x.
+    Proof. clear; induction t; rel_relb_t. Qed.
+    Definition interp_flat_type_relb_pointwise
+      := @interp_flat_type_rel_pointwise_gen_Prop bool andb true.
+    Global Arguments interp_flat_type_relb_pointwise _ !_ _ _ / .
+    Definition interp_flat_type_rel_pointwise
+      := @interp_flat_type_rel_pointwise_gen_Prop Prop and True.
+    Global Arguments interp_flat_type_rel_pointwise _ !_ _ _ / .
+    Lemma interp_flat_type_rel_pointwise_iff_relb {R} t x y
+      : interp_flat_type_relb_pointwise R t x y <-> interp_flat_type_rel_pointwise R t x y.
+    Proof. clear; induction t; rel_relb_t. Qed.
+    Definition interp_flat_type_relb_pointwise_hetero
+      := @interp_flat_type_rel_pointwise_hetero_gen_Prop bool andb true false.
+    Global Arguments interp_flat_type_relb_pointwise_hetero _ !_ !_ _ _ / .
+    Definition interp_flat_type_rel_pointwise_hetero
+      := @interp_flat_type_rel_pointwise_hetero_gen_Prop Prop and True False.
+    Global Arguments interp_flat_type_rel_pointwise_hetero _ !_ !_ _ _ / .
+    Lemma interp_flat_type_rel_pointwise_hetero_iff_relb {R} t1 t2 x y
+      : interp_flat_type_relb_pointwise_hetero R t1 t2 x y <-> interp_flat_type_rel_pointwise_hetero R t1 t2 x y.
+    Proof. clear; revert dependent t2; induction t1, t2; rel_relb_t. Qed.
+
+    Lemma interp_flat_type_rel_pointwise_hetero_iff {R t} x y
+      : interp_flat_type_rel_pointwise (fun t => R t t) t x y
+        <-> interp_flat_type_rel_pointwise_hetero R t t x y.
+    Proof. induction t; simpl; rewrite_hyp ?*; reflexivity. Qed.
+  End flat_type.
+
+  Section type.
+    Section hetero.
+      Context (interp_src1 interp_src2 : base_type_code -> Type)
+              (interp_dst1 interp_dst2 : flat_type -> Type).
       Section hetero.
-        Context (interp_src1 interp_src2 : base_type_code -> Type)
-                (interp_dst1 interp_dst2 : flat_type -> Type)
-                (Rsrc : forall t, interp_src1 t -> interp_src2 t -> Prop)
+        Context (Rsrc : forall t, interp_src1 t -> interp_src2 t -> Prop)
                 (Rdst : forall t, interp_dst1 t -> interp_dst2 t -> Prop).
 
-        Fixpoint interp_type_gen_rel_pointwise2_hetero (t : type)
+        Fixpoint interp_type_gen_rel_pointwise_hetero (t : type)
           : interp_type_gen_hetero interp_src1 interp_dst1 t
             -> interp_type_gen_hetero interp_src2 interp_dst2 t
             -> Prop
           := match t with
              | Tflat t => Rdst t
-             | Arrow src dst => @respectful_hetero _ _ _ _ (Rsrc src) (fun _ _ => interp_type_gen_rel_pointwise2_hetero dst)
+             | Arrow src dst => @respectful_hetero _ _ _ _ (Rsrc src) (fun _ _ => interp_type_gen_rel_pointwise_hetero dst)
              end.
-        Global Arguments interp_type_gen_rel_pointwise2_hetero _ _ _ / .
+        Global Arguments interp_type_gen_rel_pointwise_hetero _ _ _ / .
       End hetero.
-      Section homogenous.
-        Context (interp_flat_type1 interp_flat_type2 : flat_type -> Type)
-                (R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop).
-
-        Let Tbase := (@Tbase base_type_code).
-        Local Coercion Tbase : base_type_code >-> flat_type.
+      Section hetero_hetero.
+        Context (Rsrc : forall t1 t2, interp_src1 t1 -> interp_src2 t2 -> Prop)
+                (Rdst : forall t1 t2, interp_dst1 t1 -> interp_dst2 t2 -> Prop).
 
-        Definition interp_type_gen_rel_pointwise2
-          : forall t,
-            interp_type_gen interp_flat_type1 t
-            -> interp_type_gen interp_flat_type2 t
+        Fixpoint interp_type_gen_rel_pointwise_hetero_hetero (t1 t2 : type)
+          : interp_type_gen_hetero interp_src1 interp_dst1 t1
+            -> interp_type_gen_hetero interp_src2 interp_dst2 t2
             -> Prop
-          := interp_type_gen_rel_pointwise2_hetero interp_flat_type1 interp_flat_type2
-                                                   interp_flat_type1 interp_flat_type2
-                                                   R R.
-      End homogenous.
-      Global Arguments interp_type_gen_rel_pointwise2 _ _ _ _ _ _ / .
-    End type.
-    Section flat_type.
-      Context (interp_base_type1 interp_base_type2 : base_type_code -> Type).
-      Section gen_prop.
-        Context (P : Type)
-                (and : P -> P -> P)
-                (True : P)
-                (False : P).
-        Section hetero.
-          Context (R : forall t1 t2, interp_base_type1 t1 -> interp_base_type2 t2 -> P).
-
-          Fixpoint interp_flat_type_rel_pointwise2_hetero_gen_Prop (t1 t2 : flat_type)
-            : interp_flat_type interp_base_type1 t1 -> interp_flat_type interp_base_type2 t2 -> P
-            := match t1, t2 with
-               | Tbase t1, Tbase t2 => R t1 t2
-               | Unit, Unit => fun _ _ => True
-               | Prod x1 y1, Prod x2 y2
-                 => fun a b => and (interp_flat_type_rel_pointwise2_hetero_gen_Prop x1 x2 (fst a) (fst b))
-                                   (interp_flat_type_rel_pointwise2_hetero_gen_Prop y1 y2 (snd a) (snd b))
-               | Tbase _, _
-               | Unit, _
-               | Prod _ _, _
-                 => fun _ _ => False
-               end.
-        End hetero.
-        Section homogenous.
-          Context (R : forall t, interp_base_type1 t -> interp_base_type2 t -> P).
-
-          Fixpoint interp_flat_type_rel_pointwise2_gen_Prop (t : flat_type)
-            : interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> P
-            := match t with
-               | Tbase t => R t
-               | Unit => fun _ _ => True
-               | Prod x y => fun a b => and (interp_flat_type_rel_pointwise2_gen_Prop x (fst a) (fst b))
-                                            (interp_flat_type_rel_pointwise2_gen_Prop y (snd a) (snd b))
-               end.
-        End homogenous.
-      End gen_prop.
-
-      Definition interp_flat_type_rel_pointwise2_hetero
-        := @interp_flat_type_rel_pointwise2_hetero_gen_Prop Prop and True False.
-      Global Arguments interp_flat_type_rel_pointwise2_hetero _ !_ !_ _ _ / .
-
-      Definition interp_flat_type_rel_pointwise2
-        := @interp_flat_type_rel_pointwise2_gen_Prop Prop and True.
-      Global Arguments interp_flat_type_rel_pointwise2 _ !_ _ _ / .
+          := match t1, t2 with
+             | Tflat t1, Tflat t2 => Rdst t1 t2
+             | Arrow src1 dst1, Arrow src2 dst2
+               => @respectful_hetero _ _ _ _ (Rsrc src1 src2) (fun _ _ => interp_type_gen_rel_pointwise_hetero_hetero dst1 dst2)
+             | Tflat _, _
+             | Arrow _ _, _
+               => fun _ _ => False
+             end.
+        Global Arguments interp_type_gen_rel_pointwise_hetero_hetero _ _ _ _ / .
+      End hetero_hetero.
+    End hetero.
 
-      Lemma interp_flat_type_rel_pointwise2_hetero_iff {R t} x y
-        : interp_flat_type_rel_pointwise2 (fun t => R t t) t x y
-          <-> interp_flat_type_rel_pointwise2_hetero R t t x y.
-      Proof. induction t; simpl; rewrite_hyp ?*; reflexivity. Qed.
+    Section partially_hetero.
+      Context (interp_flat_type1 interp_flat_type2 : flat_type -> Type)
+              (R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop).
 
-      Section with_coercion.
-        Let Tbase := (@Tbase base_type_code).
-        Local Coercion Tbase : base_type_code >-> flat_type.
+      Definition interp_type_gen_rel_pointwise2
+        : forall t,
+          interp_type_gen interp_flat_type1 t
+          -> interp_type_gen interp_flat_type2 t
+          -> Prop
+        := interp_type_gen_rel_pointwise_hetero
+             (fun t => interp_flat_type1 (Tbase t)) (fun t => interp_flat_type2 (Tbase t))
+             interp_flat_type1 interp_flat_type2
+             (fun t => R (Tbase t)) R.
+      Global Arguments interp_type_gen_rel_pointwise2 _ _ _ / .
+    End partially_hetero.
 
-        Definition interp_type_rel_pointwise2_hetero R
-          : forall t1 t2, interp_type interp_base_type1 t1
-                          -> interp_type interp_base_type2 t2
-                          -> Prop
-          := interp_type_gen_rel_pointwise2_hetero_hetero _ _ _ _ (interp_flat_type_rel_pointwise2_hetero R) (interp_flat_type_rel_pointwise2_hetero R).
-      End with_coercion.
-      Global Arguments interp_type_rel_pointwise2_hetero _ !_ !_ _ _ / .
+    Section homogenous.
+      Context (interp_flat_type : flat_type -> Type)
+              (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop).
+      Local Notation interp_type_gen := (interp_type_gen interp_flat_type).
+      Fixpoint interp_type_gen_rel_pointwise (t : type)
+        : interp_type_gen t -> interp_type_gen t -> Prop :=
+        match t with
+        | Tflat t => R t
+        | Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x)
+        end.
+      Global Instance interp_type_gen_rel_pointwise_Reflexive {H : forall t, Reflexive (R t)}
+        : forall t, Reflexive (interp_type_gen_rel_pointwise t).
+      Proof. induction t; repeat intro; reflexivity. Qed.
+      Global Instance interp_type_gen_rel_pointwise_Symmetric {H : forall t, Symmetric (R t)}
+        : forall t, Symmetric (interp_type_gen_rel_pointwise t).
+      Proof. induction t; simpl; repeat intro; symmetry; eauto. Qed.
+      Global Instance interp_type_gen_rel_pointwise_Transitive {H : forall t, Transitive (R t)}
+        : forall t, Transitive (interp_type_gen_rel_pointwise t).
+      Proof. induction t; simpl; repeat intro; etransitivity; eauto. Qed.
+    End homogenous.
+  End type.
 
+  Section specialized_type.
+    Section hetero.
+      Context (interp_base_type1 interp_base_type2 : base_type_code -> Type).
       Definition interp_type_rel_pointwise2 R
         : forall t, interp_type interp_base_type1 t
                     -> interp_type interp_base_type2 t
                     -> Prop
-        := interp_type_gen_rel_pointwise2 _ _ (interp_flat_type_rel_pointwise2 R).
+        := interp_type_gen_rel_pointwise2 _ _ (interp_flat_type_rel_pointwise R).
       Global Arguments interp_type_rel_pointwise2 _ !_ _ _ / .
-    End flat_type.
-  End rel_pointwise2.
+
+      Definition interp_type_rel_pointwise2_hetero R
+        : forall t1 t2, interp_type interp_base_type1 t1
+                        -> interp_type interp_base_type2 t2
+                        -> Prop
+        := interp_type_gen_rel_pointwise_hetero_hetero _ _ _ _ (fun t1 t2 => interp_flat_type_rel_pointwise_hetero R (Tbase t1) (Tbase t2)) (interp_flat_type_rel_pointwise_hetero R).
+      Global Arguments interp_type_rel_pointwise2_hetero _ !_ !_ _ _ / .
+    End hetero.
+
+    Section homogenous.
+      Context {interp_base_type : base_type_code -> Type}.
+      Definition interp_type_rel_pointwise R
+        := interp_type_gen_rel_pointwise _ (@interp_flat_type_rel_pointwise interp_base_type interp_base_type R).
+    End homogenous.
+  End specialized_type.
 
   Section lifting.
+    Context {interp_base_type1 interp_base_type2 : base_type_code -> Type}.
+    Local Notation interp_flat_type1 := (interp_flat_type interp_base_type1).
+    Local Notation interp_flat_type2 := (interp_flat_type interp_base_type2).
     Let Tbase := (@Tbase base_type_code).
     Local Coercion Tbase : base_type_code >-> flat_type.
 
-    Section flat_type.
-      Context {interp_base_type : base_type_code -> Type}.
-      Local Notation interp_flat_type := (interp_flat_type interp_base_type).
-      Context (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop)
+    Section with_rel.
+      Context (R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop)
               (RUnit : R Unit tt tt).
       Section RProd.
         Context (RProd : forall A B x y, R A (fst x) (fst y) /\ R B (snd x) (snd y) -> R (Prod A B) x y)
                 (RProd' : forall A B x y, R (Prod A B) x y -> R A (fst x) (fst y) /\ R B (snd x) (snd y)).
-        Lemma lift_interp_flat_type_rel_pointwise1 t (x y : interp_flat_type t)
+        Lemma lift_interp_flat_type_rel_pointwise1 t (x : interp_flat_type1 t) (y : interp_flat_type2 t)
           : interp_flat_type_rel_pointwise R t x y -> R t x y.
         Proof. clear RProd'; induction t; simpl; destruct_head_hnf' unit; intuition. Qed.
-        Lemma lift_interp_flat_type_rel_pointwise2 t (x y : interp_flat_type t)
+        Lemma lift_interp_flat_type_rel_pointwise2 t (x : interp_flat_type1 t) (y : interp_flat_type2 t)
           : R t x y -> interp_flat_type_rel_pointwise R t x y.
         Proof. clear RProd; induction t; simpl; destruct_head_hnf' unit; split_and; intuition. Qed.
       End RProd.
       Section RProd_iff.
         Context (RProd : forall A B x y, R A (fst x) (fst y) /\ R B (snd x) (snd y) <-> R (Prod A B) x y).
-        Lemma lift_interp_flat_type_rel_pointwise t (x y : interp_flat_type t)
+        Lemma lift_interp_flat_type_rel_pointwise t (x : interp_flat_type1 t) (y : interp_flat_type2 t)
           : interp_flat_type_rel_pointwise R t x y <-> R t x y.
         Proof.
           split_iff; split; auto using lift_interp_flat_type_rel_pointwise1, lift_interp_flat_type_rel_pointwise2.
         Qed.
       End RProd_iff.
-    End flat_type.
-    Section flat_type2.
-      Context {interp_base_type1 interp_base_type2 : base_type_code -> Type}.
-      Lemma lift_interp_flat_type_rel_pointwise2_f_eq {T} (f g : forall t, _ -> T t) t x y
-        : interp_flat_type_rel_pointwise2
-            interp_base_type1 interp_base_type2
-            (fun t x y => f t x = g t y)
-            t x y
-          <-> SmartVarfMap f x = SmartVarfMap g y.
-      Proof.
-        induction t; unfold SmartVarfMap in *; simpl in *; destruct_head_hnf unit; try tauto.
-        rewrite_hyp !*; intuition congruence.
-      Qed.
-      Lemma lift_interp_flat_type_rel_pointwise2_f_eq_id1 (f : forall t, _ -> _) t x y
-        : interp_flat_type_rel_pointwise2
-            interp_base_type1 interp_base_type2
-            (fun t x y => x = f t y)
-            t x y
-          <-> x = SmartVarfMap f y.
-      Proof. rewrite lift_interp_flat_type_rel_pointwise2_f_eq, SmartVarfMap_id; reflexivity. Qed.
-      Lemma lift_interp_flat_type_rel_pointwise2_f_eq_id2 (f : forall t, _ -> _) t x y
-        : interp_flat_type_rel_pointwise2
-            interp_base_type1 interp_base_type2
-            (fun t x y => f t x = y)
-            t x y
-          <-> SmartVarfMap f x = y.
-      Proof. rewrite lift_interp_flat_type_rel_pointwise2_f_eq, SmartVarfMap_id; reflexivity. Qed.
-    End flat_type2.
+    End with_rel.
+    Lemma lift_interp_flat_type_rel_pointwise_f_eq {T} (f g : forall t, _ -> T t) t x y
+      : @interp_flat_type_rel_pointwise
+          interp_base_type1 interp_base_type2
+          (fun t x y => f t x = g t y)
+          t x y
+        <-> SmartVarfMap f x = SmartVarfMap g y.
+    Proof.
+      induction t; unfold SmartVarfMap in *; simpl in *; destruct_head_hnf unit; try tauto.
+      rewrite_hyp !*; intuition congruence.
+    Qed.
+    Lemma lift_interp_flat_type_rel_pointwise_f_eq_id1 (f : forall t, _ -> _) t x y
+      : @interp_flat_type_rel_pointwise
+          interp_base_type1 interp_base_type2
+          (fun t x y => x = f t y)
+          t x y
+        <-> x = SmartVarfMap f y.
+    Proof. rewrite lift_interp_flat_type_rel_pointwise_f_eq, SmartVarfMap_id; reflexivity. Qed.
+    Lemma lift_interp_flat_type_rel_pointwise_f_eq_id2 (f : forall t, _ -> _) t x y
+      : @interp_flat_type_rel_pointwise
+          interp_base_type1 interp_base_type2
+          (fun t x y => f t x = y)
+          t x y
+        <-> SmartVarfMap f x = y.
+    Proof. rewrite lift_interp_flat_type_rel_pointwise_f_eq, SmartVarfMap_id; reflexivity. Qed.
   End lifting.
 
   Local Ltac t :=
@@ -265,17 +279,17 @@ Section language.
            | _ => solve [ eauto ]
            end.
 
-  Lemma interp_flat_type_rel_pointwise2_flatten_binding_list
+  Lemma interp_flat_type_rel_pointwise_flatten_binding_list
         {interp_base_type1 interp_base_type2 t T} R' e1 e2 v1 v2
         (H : List.In (existT _ t (v1, v2)%core) (flatten_binding_list e1 e2))
-        (HR : interp_flat_type_rel_pointwise2 interp_base_type1 interp_base_type2 R' T e1 e2)
+        (HR : @interp_flat_type_rel_pointwise interp_base_type1 interp_base_type2 R' T e1 e2)
     : R' t v1 v2.
   Proof. induction T; t. Qed.
 
-  Lemma interp_flat_type_rel_pointwise2_hetero_flatten_binding_list2
+  Lemma interp_flat_type_rel_pointwise_hetero_flatten_binding_list2
         {interp_base_type1 interp_base_type2 t1 t2 T1 T2} R' e1 e2 v1 v2
         (H : List.In (existT _ (t1, t2)%core (v1, v2)%core) (flatten_binding_list2 e1 e2))
-        (HR : interp_flat_type_rel_pointwise2_hetero interp_base_type1 interp_base_type2 R' T1 T2 e1 e2)
+        (HR : @interp_flat_type_rel_pointwise_hetero interp_base_type1 interp_base_type2 R' T1 T2 e1 e2)
     : R' t1 t2 v1 v2.
   Proof.
     revert dependent T2; induction T1, T2; t.
@@ -284,15 +298,13 @@ End language.
 
 Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _.
 Global Arguments interp_type_rel_pointwise2_hetero {_ _ _} R {t1 t2} _ _.
-Global Arguments interp_type_gen_rel_pointwise2_hetero_hetero {_ _ _ _ _} Rsrc Rdst {t1 t2} _ _.
-Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc Rdst {t} _ _.
+Global Arguments interp_type_gen_rel_pointwise_hetero_hetero {_ _ _ _ _} Rsrc Rdst {t1 t2} _ _.
+Global Arguments interp_type_gen_rel_pointwise_hetero {_ _ _ _ _} Rsrc Rdst {t} _ _.
 Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _.
-Global Arguments interp_flat_type_rel_pointwise2_gen_Prop {_ _ _ P} and True R {t} _ _.
-Global Arguments interp_flat_type_rel_pointwise2_hetero_gen_Prop {_ _ _ P} and True False R {t1 t2} _ _.
-Global Arguments interp_flat_type_rel_pointwise2_hetero {_ _ _} R {t1 t2} _ _.
-Global Arguments interp_flat_type_rel_pointwise0 {_ _} R {t} _.
-Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _.
-Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _.
+Global Arguments interp_flat_type_rel_pointwise_gen_Prop {_ _ _ P} and True R {t} _ _.
+Global Arguments interp_flat_type_rel_pointwise_hetero_gen_Prop {_ _ _ P} and True False R {t1 t2} _ _.
+Global Arguments interp_flat_type_rel_pointwise_hetero {_ _ _} R {t1 t2} _ _.
+Global Arguments interp_flat_type_rel_pointwise1 {_ _} R {t} _.
+Global Arguments interp_flat_type_rel_pointwise {_ _ _} R {t} _ _.
 Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _.
 Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _.
-Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _.
diff --git a/src/Reflection/Z/Interpretations128/Relations.v b/src/Reflection/Z/Interpretations128/Relations.v
index 2a7db515a..7f6f67fa2 100644
--- a/src/Reflection/Z/Interpretations128/Relations.v
+++ b/src/Reflection/Z/Interpretations128/Relations.v
@@ -49,8 +49,8 @@ Definition related_wordW_boundsi' (t : base_type) : ZBounds.bounds -> WordW.inte
 Local Notation related_op R interp_op1 interp_op2
   := (forall (src dst : flat_type base_type) (op : op src dst)
              (sv1 : interp_flat_type _ src) (sv2 : interp_flat_type _ src),
-         interp_flat_type_rel_pointwise2 R sv1 sv2 ->
-         interp_flat_type_rel_pointwise2 R (interp_op1 _ _ op sv1) (interp_op2 _ _ op sv2))
+         interp_flat_type_rel_pointwise R sv1 sv2 ->
+         interp_flat_type_rel_pointwise R (interp_op1 _ _ op sv1) (interp_op2 _ _ op sv2))
        (only parsing).
 Local Notation related_const R interp f g
   := (forall (t : base_type) (v : interp t), R t (f t v) (g t v))
@@ -121,29 +121,29 @@ Local Ltac related_wordW_op_t := repeat related_wordW_op_t_step.
 
 Lemma related_wordW_t_map1 opW opB pf
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_wordW sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Tbase TZ) related_wordW sv1 sv2
     -> @related_wordW TZ (BoundedWordW.t_map1 opW opB pf sv1) (opW sv2).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
 Lemma related_wordW_t_map2 opW opB pf
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Tbase TZ) (Tbase TZ)) related_wordW sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Tbase TZ) (Tbase TZ)) related_wordW sv1 sv2
     -> @related_wordW TZ (BoundedWordW.t_map2 opW opB pf (fst sv1) (snd sv1)) (opW (fst sv2) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
 Lemma related_wordW_t_map4 opW opB pf
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_wordW sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_wordW sv1 sv2
     -> @related_wordW TZ (BoundedWordW.t_map4 opW opB pf (fst (fst (fst sv1))) (snd (fst (fst sv1))) (snd (fst sv1)) (snd sv1))
                        (opW (fst (fst (fst sv2))) (snd (fst (fst sv2))) (snd (fst sv2)) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
@@ -152,7 +152,7 @@ Lemma related_tuples_None_left
       (R : forall t, LiftOption.interp_base_type' T t -> interp_base_type' t -> Prop)
       (RNone : forall v, R TZ None v)
       (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n)))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       R
       (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option None))
       v.
@@ -165,11 +165,11 @@ Lemma related_tuples_Some_left
       (R : forall t, T -> interp_base_type' t -> Prop)
       u
       (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) n))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       R
       (flat_interp_untuple (T:=Tbase TZ) u)
       v
-    <-> interp_flat_type_rel_pointwise2
+    <-> interp_flat_type_rel_pointwise
           (LiftOption.lift_relation R)
           (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option (Some u)))
           v.
@@ -185,10 +185,10 @@ Lemma related_tuples_Some_left_ext
       {R : forall t, T -> interp_base_type' t -> Prop}
       {u v u'}
       (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=n) u) = Some u')
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       R
       (flat_interp_untuple (T:=Tbase TZ) u') v
-    <-> interp_flat_type_rel_pointwise2
+    <-> interp_flat_type_rel_pointwise
           (LiftOption.lift_relation R)
           u v.
 Proof.
@@ -205,7 +205,7 @@ Lemma related_tuples_proj_eq_rel_untuple
       {n T interp_base_type'}
       {proj : forall t, T -> interp_base_type' t}
       {u : Tuple.tuple _ n} {v : Tuple.tuple _ n}
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (fun t => proj_eq_rel (proj t))
       (flat_interp_untuple (T:=Tbase TZ) u)
       (flat_interp_untuple (T:=Tbase TZ) v)
@@ -224,7 +224,7 @@ Lemma related_tuples_proj_eq_rel_tuple
       {n T interp_base_type'}
       {proj : forall t, T -> interp_base_type' t}
       {u v}
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (fun t => proj_eq_rel (proj t))
       u v
     <-> (Tuple.map (proj _) (flat_interp_tuple (n:=n) (T:=Tbase TZ) u)
@@ -239,12 +239,12 @@ Lemma related_tuples_lift_relation2_untuple
       (R : T -> U -> Prop)
       (t : option (Tuple.tuple T (S n)))
       (u : option (Tuple.tuple U (S n)))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (LiftOption.lift_relation2 R)
       (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option t))
       (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option u))
     <-> LiftOption.lift_relation2
-          (interp_flat_type_rel_pointwise2 (fun _ => R))
+          (interp_flat_type_rel_pointwise (fun _ => R))
           TZ
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
@@ -257,7 +257,7 @@ Proof.
       simpl @option_map in *;
       simpl @LiftOption.lift_relation2 in *;
       try (rewrite <- IHn; reflexivity);
-      try (simpl @interp_flat_type_rel_pointwise2; tauto). }
+      try (simpl @interp_flat_type_rel_pointwise; tauto). }
 Qed.
 
 Lemma related_tuples_lift_relation2_untuple_ext
@@ -266,11 +266,11 @@ Lemma related_tuples_lift_relation2_untuple_ext
       {t u}
       (H : (exists v, Tuple.lift_option (n:=S n) (flat_interp_tuple (T:=Tbase TZ) t) = Some v)
            \/ (exists v, Tuple.lift_option (n:=S n) (flat_interp_tuple (T:=Tbase TZ) u) = Some v))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (LiftOption.lift_relation2 R)
       t u
     <-> LiftOption.lift_relation2
-          (interp_flat_type_rel_pointwise2 (fun _ => R))
+          (interp_flat_type_rel_pointwise (fun _ => R))
           TZ
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
@@ -289,7 +289,7 @@ Proof.
     destruct_head_hnf' prod;
       destruct_head_hnf' option;
       simpl @fst in *; simpl @snd in *;
-        (etransitivity; [ simpl @interp_flat_type_rel_pointwise2 | reflexivity ]);
+        (etransitivity; [ simpl @interp_flat_type_rel_pointwise | reflexivity ]);
         try solve [ repeat first [ progress simpl in *
                                  | tauto
                                  | congruence
@@ -309,9 +309,9 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma lift_option_None_interp_flat_type_rel_pointwise2_1
+Lemma lift_option_None_interp_flat_type_rel_pointwise_1
       T U n R x y
-      (H : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) x y)
+      (H : interp_flat_type_rel_pointwise (LiftOption.lift_relation2 R) x y)
       (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) x) = None)
   : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) y) = None.
 Proof.
@@ -350,10 +350,10 @@ Qed.
 Lemma related_bounds_t_map1 opW opB pf
       (HN : opB None = None)
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_bounds sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Tbase TZ) related_bounds sv1 sv2
     -> @related_bounds TZ (BoundedWordW.t_map1 opW opB pf sv1) (opB sv2).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
@@ -361,10 +361,10 @@ Lemma related_bounds_t_map2 opW opB pf
       (HN0 : forall v, opB None v = None)
       (HN1 : forall v, opB v None = None)
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Tbase TZ) (Tbase TZ)) related_bounds sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Tbase TZ) (Tbase TZ)) related_bounds sv1 sv2
     -> @related_bounds TZ (BoundedWordW.t_map2 opW opB pf (fst sv1) (snd sv1)) (opB (fst sv2) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
@@ -374,11 +374,11 @@ Lemma related_bounds_t_map4 opW opB pf
       (HN2 : forall x y z, opB x y None z = None)
       (HN3 : forall x y z, opB x y z None = None)
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_bounds sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_bounds sv1 sv2
     -> @related_bounds TZ (BoundedWordW.t_map4 opW opB pf (fst (fst (fst sv1))) (snd (fst (fst sv1))) (snd (fst sv1)) (snd sv1))
                        (opB (fst (fst (fst sv2))) (snd (fst (fst sv2))) (snd (fst sv2)) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   destruct_head prod.
   intros; destruct_head' prod.
   progress cbv [related_wordW related_bounds related_Z LiftOption.lift_relation LiftOption.lift_relation2 LiftOption.of' smart_interp_flat_map BoundedWordW.BoundedWordToBounds BoundedWordW.to_bounds' proj_eq_rel] in *.
@@ -467,10 +467,10 @@ Lemma related_Z_t_map1 opZ opW opB pf
           -> is_in_bounds (opW x) brs
           -> WordW.wordWToZ (opW x) = (opZ (WordW.wordWToZ x)))
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_Z sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Tbase TZ) related_Z sv1 sv2
     -> @related_Z TZ (BoundedWordW.t_map1 opW opB pf sv1) (opZ sv2).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_Z_op_t.
   eapply H; eauto.
 Qed.
@@ -483,10 +483,10 @@ Lemma related_Z_t_map2 opZ opW opB pf
           -> is_in_bounds (opW x y) brs
           -> WordW.wordWToZ (opW x y) = (opZ (WordW.wordWToZ x) (WordW.wordWToZ y)))
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Tbase TZ) (Tbase TZ)) related_Z sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Tbase TZ) (Tbase TZ)) related_Z sv1 sv2
     -> @related_Z TZ (BoundedWordW.t_map2 opW opB pf (fst sv1) (snd sv1)) (opZ (fst sv2) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_Z_op_t.
   eapply H; eauto.
 Qed.
@@ -501,11 +501,11 @@ Lemma related_Z_t_map4 opZ opW opB pf
           -> is_in_bounds (opW x y z w) brs
           -> WordW.wordWToZ (opW x y z w) = (opZ (WordW.wordWToZ x) (WordW.wordWToZ y) (WordW.wordWToZ z) (WordW.wordWToZ w)))
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=(Tbase TZ * Tbase TZ * Tbase TZ * Tbase TZ)%ctype) related_Z sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=(Tbase TZ * Tbase TZ * Tbase TZ * Tbase TZ)%ctype) related_Z sv1 sv2
     -> @related_Z TZ (BoundedWordW.t_map4 opW opB pf (fst (fst (fst sv1))) (snd (fst (fst sv1))) (snd (fst sv1)) (snd sv1))
                   (opZ (fst (fst (fst sv2))) (snd (fst (fst sv2))) (snd (fst sv2)) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_Z_op_t.
   eapply H; eauto.
 Qed.
diff --git a/src/Reflection/Z/Interpretations128/RelationsCombinations.v b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
index d5c07513d..68fca675e 100644
--- a/src/Reflection/Z/Interpretations128/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
@@ -21,11 +21,11 @@ Module Relations.
     Definition interp_type_rel_pointwise2_uncurried
                {t : type base_type}
       := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> _ with
-         | Tflat T => fun f g => interp_flat_type_rel_pointwise2 (t:=T) R f g
+         | Tflat T => fun f g => interp_flat_type_rel_pointwise (t:=T) R f g
          | Arrow A B
            => fun f g
-              => forall x y, interp_flat_type_rel_pointwise2 R x y
-                             -> interp_flat_type_rel_pointwise2 R (ApplyInterpedAll f x) (ApplyInterpedAll g y)
+              => forall x y, interp_flat_type_rel_pointwise R x y
+                             -> interp_flat_type_rel_pointwise R (ApplyInterpedAll f x) (ApplyInterpedAll g y)
          end.
 
     Lemma uncurry_interp_type_rel_pointwise2
@@ -290,7 +290,7 @@ Module Relations.
                                     | Some _ => True
                                     | None => False
                                     end -> match LiftOption.of' f with
-                                           | Some f' => interp_flat_type_rel_pointwise2 (@R) f' g
+                                           | Some f' => interp_flat_type_rel_pointwise (@R) f' g
                                            | None => True
                                            end
          | Arrow A B
@@ -306,7 +306,7 @@ Module Relations.
                   | None => False
                   end
                   -> match fx with
-                     | Some fx' => interp_flat_type_rel_pointwise2 (@R) fx' gy
+                     | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy
                      | None => True
                      end
          end.
@@ -354,9 +354,9 @@ Module Relations.
           {R3 : forall t : base_type, interp_base_type2 t -> interp_base_type3 t -> Prop}
           {t x y z}
     : (forall t a b c, (R1 t a b : Prop) -> (R2 t a c : Prop) -> (R3 t b c : Prop))
-      -> interp_flat_type_rel_pointwise2 (t:=t) R1 x y
-      -> interp_flat_type_rel_pointwise2 (t:=t) R2 x z
-      -> interp_flat_type_rel_pointwise2 (t:=t) R3 y z.
+      -> interp_flat_type_rel_pointwise (t:=t) R1 x y
+      -> interp_flat_type_rel_pointwise (t:=t) R2 x z
+      -> interp_flat_type_rel_pointwise (t:=t) R3 y z.
     Proof.
       intro HRel; induction t; simpl; intuition eauto.
     Qed.
diff --git a/src/Reflection/Z/Interpretations64/Relations.v b/src/Reflection/Z/Interpretations64/Relations.v
index 525ecd266..02934c46a 100644
--- a/src/Reflection/Z/Interpretations64/Relations.v
+++ b/src/Reflection/Z/Interpretations64/Relations.v
@@ -49,8 +49,8 @@ Definition related_wordW_boundsi' (t : base_type) : ZBounds.bounds -> WordW.inte
 Local Notation related_op R interp_op1 interp_op2
   := (forall (src dst : flat_type base_type) (op : op src dst)
              (sv1 : interp_flat_type _ src) (sv2 : interp_flat_type _ src),
-         interp_flat_type_rel_pointwise2 R sv1 sv2 ->
-         interp_flat_type_rel_pointwise2 R (interp_op1 _ _ op sv1) (interp_op2 _ _ op sv2))
+         interp_flat_type_rel_pointwise R sv1 sv2 ->
+         interp_flat_type_rel_pointwise R (interp_op1 _ _ op sv1) (interp_op2 _ _ op sv2))
        (only parsing).
 Local Notation related_const R interp f g
   := (forall (t : base_type) (v : interp t), R t (f t v) (g t v))
@@ -121,29 +121,29 @@ Local Ltac related_wordW_op_t := repeat related_wordW_op_t_step.
 
 Lemma related_wordW_t_map1 opW opB pf
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_wordW sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Tbase TZ) related_wordW sv1 sv2
     -> @related_wordW TZ (BoundedWordW.t_map1 opW opB pf sv1) (opW sv2).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
 Lemma related_wordW_t_map2 opW opB pf
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Tbase TZ) (Tbase TZ)) related_wordW sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Tbase TZ) (Tbase TZ)) related_wordW sv1 sv2
     -> @related_wordW TZ (BoundedWordW.t_map2 opW opB pf (fst sv1) (snd sv1)) (opW (fst sv2) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
 Lemma related_wordW_t_map4 opW opB pf
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_wordW sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_wordW sv1 sv2
     -> @related_wordW TZ (BoundedWordW.t_map4 opW opB pf (fst (fst (fst sv1))) (snd (fst (fst sv1))) (snd (fst sv1)) (snd sv1))
                        (opW (fst (fst (fst sv2))) (snd (fst (fst sv2))) (snd (fst sv2)) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
@@ -152,7 +152,7 @@ Lemma related_tuples_None_left
       (R : forall t, LiftOption.interp_base_type' T t -> interp_base_type' t -> Prop)
       (RNone : forall v, R TZ None v)
       (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n)))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       R
       (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option None))
       v.
@@ -165,11 +165,11 @@ Lemma related_tuples_Some_left
       (R : forall t, T -> interp_base_type' t -> Prop)
       u
       (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) n))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       R
       (flat_interp_untuple (T:=Tbase TZ) u)
       v
-    <-> interp_flat_type_rel_pointwise2
+    <-> interp_flat_type_rel_pointwise
           (LiftOption.lift_relation R)
           (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option (Some u)))
           v.
@@ -185,10 +185,10 @@ Lemma related_tuples_Some_left_ext
       {R : forall t, T -> interp_base_type' t -> Prop}
       {u v u'}
       (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=n) u) = Some u')
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       R
       (flat_interp_untuple (T:=Tbase TZ) u') v
-    <-> interp_flat_type_rel_pointwise2
+    <-> interp_flat_type_rel_pointwise
           (LiftOption.lift_relation R)
           u v.
 Proof.
@@ -205,7 +205,7 @@ Lemma related_tuples_proj_eq_rel_untuple
       {n T interp_base_type'}
       {proj : forall t, T -> interp_base_type' t}
       {u : Tuple.tuple _ n} {v : Tuple.tuple _ n}
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (fun t => proj_eq_rel (proj t))
       (flat_interp_untuple (T:=Tbase TZ) u)
       (flat_interp_untuple (T:=Tbase TZ) v)
@@ -224,7 +224,7 @@ Lemma related_tuples_proj_eq_rel_tuple
       {n T interp_base_type'}
       {proj : forall t, T -> interp_base_type' t}
       {u v}
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (fun t => proj_eq_rel (proj t))
       u v
     <-> (Tuple.map (proj _) (flat_interp_tuple (n:=n) (T:=Tbase TZ) u)
@@ -239,12 +239,12 @@ Lemma related_tuples_lift_relation2_untuple
       (R : T -> U -> Prop)
       (t : option (Tuple.tuple T (S n)))
       (u : option (Tuple.tuple U (S n)))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (LiftOption.lift_relation2 R)
       (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option t))
       (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option u))
     <-> LiftOption.lift_relation2
-          (interp_flat_type_rel_pointwise2 (fun _ => R))
+          (interp_flat_type_rel_pointwise (fun _ => R))
           TZ
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
@@ -257,7 +257,7 @@ Proof.
       simpl @option_map in *;
       simpl @LiftOption.lift_relation2 in *;
       try (rewrite <- IHn; reflexivity);
-      try (simpl @interp_flat_type_rel_pointwise2; tauto). }
+      try (simpl @interp_flat_type_rel_pointwise; tauto). }
 Qed.
 
 Lemma related_tuples_lift_relation2_untuple_ext
@@ -266,11 +266,11 @@ Lemma related_tuples_lift_relation2_untuple_ext
       {t u}
       (H : (exists v, Tuple.lift_option (n:=S n) (flat_interp_tuple (T:=Tbase TZ) t) = Some v)
            \/ (exists v, Tuple.lift_option (n:=S n) (flat_interp_tuple (T:=Tbase TZ) u) = Some v))
-  : interp_flat_type_rel_pointwise2
+  : interp_flat_type_rel_pointwise
       (LiftOption.lift_relation2 R)
       t u
     <-> LiftOption.lift_relation2
-          (interp_flat_type_rel_pointwise2 (fun _ => R))
+          (interp_flat_type_rel_pointwise (fun _ => R))
           TZ
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
           (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
@@ -289,7 +289,7 @@ Proof.
     destruct_head_hnf' prod;
       destruct_head_hnf' option;
       simpl @fst in *; simpl @snd in *;
-        (etransitivity; [ simpl @interp_flat_type_rel_pointwise2 | reflexivity ]);
+        (etransitivity; [ simpl @interp_flat_type_rel_pointwise | reflexivity ]);
         try solve [ repeat first [ progress simpl in *
                                  | tauto
                                  | congruence
@@ -309,9 +309,9 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma lift_option_None_interp_flat_type_rel_pointwise2_1
+Lemma lift_option_None_interp_flat_type_rel_pointwise_1
       T U n R x y
-      (H : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) x y)
+      (H : interp_flat_type_rel_pointwise (LiftOption.lift_relation2 R) x y)
       (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) x) = None)
   : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) y) = None.
 Proof.
@@ -350,10 +350,10 @@ Qed.
 Lemma related_bounds_t_map1 opW opB pf
       (HN : opB None = None)
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_bounds sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Tbase TZ) related_bounds sv1 sv2
     -> @related_bounds TZ (BoundedWordW.t_map1 opW opB pf sv1) (opB sv2).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
@@ -361,10 +361,10 @@ Lemma related_bounds_t_map2 opW opB pf
       (HN0 : forall v, opB None v = None)
       (HN1 : forall v, opB v None = None)
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Tbase TZ) (Tbase TZ)) related_bounds sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Tbase TZ) (Tbase TZ)) related_bounds sv1 sv2
     -> @related_bounds TZ (BoundedWordW.t_map2 opW opB pf (fst sv1) (snd sv1)) (opB (fst sv2) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_wordW_op_t.
 Qed.
 
@@ -374,11 +374,11 @@ Lemma related_bounds_t_map4 opW opB pf
       (HN2 : forall x y z, opB x y None z = None)
       (HN3 : forall x y z, opB x y z None = None)
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_bounds sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Prod (Prod (Tbase TZ) (Tbase TZ)) (Tbase TZ)) (Tbase TZ)) related_bounds sv1 sv2
     -> @related_bounds TZ (BoundedWordW.t_map4 opW opB pf (fst (fst (fst sv1))) (snd (fst (fst sv1))) (snd (fst sv1)) (snd sv1))
                        (opB (fst (fst (fst sv2))) (snd (fst (fst sv2))) (snd (fst sv2)) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   destruct_head prod.
   intros; destruct_head' prod.
   progress cbv [related_wordW related_bounds related_Z LiftOption.lift_relation LiftOption.lift_relation2 LiftOption.of' smart_interp_flat_map BoundedWordW.BoundedWordToBounds BoundedWordW.to_bounds' proj_eq_rel] in *.
@@ -467,10 +467,10 @@ Lemma related_Z_t_map1 opZ opW opB pf
           -> is_in_bounds (opW x) brs
           -> WordW.wordWToZ (opW x) = (opZ (WordW.wordWToZ x)))
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_Z sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Tbase TZ) related_Z sv1 sv2
     -> @related_Z TZ (BoundedWordW.t_map1 opW opB pf sv1) (opZ sv2).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_Z_op_t.
   eapply H; eauto.
 Qed.
@@ -483,10 +483,10 @@ Lemma related_Z_t_map2 opZ opW opB pf
           -> is_in_bounds (opW x y) brs
           -> WordW.wordWToZ (opW x y) = (opZ (WordW.wordWToZ x) (WordW.wordWToZ y)))
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=Prod (Tbase TZ) (Tbase TZ)) related_Z sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=Prod (Tbase TZ) (Tbase TZ)) related_Z sv1 sv2
     -> @related_Z TZ (BoundedWordW.t_map2 opW opB pf (fst sv1) (snd sv1)) (opZ (fst sv2) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_Z_op_t.
   eapply H; eauto.
 Qed.
@@ -501,11 +501,11 @@ Lemma related_Z_t_map4 opZ opW opB pf
           -> is_in_bounds (opW x y z w) brs
           -> WordW.wordWToZ (opW x y z w) = (opZ (WordW.wordWToZ x) (WordW.wordWToZ y) (WordW.wordWToZ z) (WordW.wordWToZ w)))
       sv1 sv2
-  : interp_flat_type_rel_pointwise2 (t:=(Tbase TZ * Tbase TZ * Tbase TZ * Tbase TZ)%ctype) related_Z sv1 sv2
+  : interp_flat_type_rel_pointwise (t:=(Tbase TZ * Tbase TZ * Tbase TZ * Tbase TZ)%ctype) related_Z sv1 sv2
     -> @related_Z TZ (BoundedWordW.t_map4 opW opB pf (fst (fst (fst sv1))) (snd (fst (fst sv1))) (snd (fst sv1)) (snd sv1))
                   (opZ (fst (fst (fst sv2))) (snd (fst (fst sv2))) (snd (fst sv2)) (snd sv2)).
 Proof.
-  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  cbv [interp_flat_type BoundedWordW.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise interp_flat_type_rel_pointwise_gen_Prop] in *.
   related_Z_op_t.
   eapply H; eauto.
 Qed.
diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
index d4a125499..3a95bcc51 100644
--- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
@@ -21,11 +21,11 @@ Module Relations.
     Definition interp_type_rel_pointwise2_uncurried
                {t : type base_type}
       := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> _ with
-         | Tflat T => fun f g => interp_flat_type_rel_pointwise2 (t:=T) R f g
+         | Tflat T => fun f g => interp_flat_type_rel_pointwise (t:=T) R f g
          | Arrow A B
            => fun f g
-              => forall x y, interp_flat_type_rel_pointwise2 R x y
-                             -> interp_flat_type_rel_pointwise2 R (ApplyInterpedAll f x) (ApplyInterpedAll g y)
+              => forall x y, interp_flat_type_rel_pointwise R x y
+                             -> interp_flat_type_rel_pointwise R (ApplyInterpedAll f x) (ApplyInterpedAll g y)
          end.
 
     Lemma uncurry_interp_type_rel_pointwise2
@@ -290,7 +290,7 @@ Module Relations.
                                     | Some _ => True
                                     | None => False
                                     end -> match LiftOption.of' f with
-                                           | Some f' => interp_flat_type_rel_pointwise2 (@R) f' g
+                                           | Some f' => interp_flat_type_rel_pointwise (@R) f' g
                                            | None => True
                                            end
          | Arrow A B
@@ -306,7 +306,7 @@ Module Relations.
                   | None => False
                   end
                   -> match fx with
-                     | Some fx' => interp_flat_type_rel_pointwise2 (@R) fx' gy
+                     | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy
                      | None => True
                      end
          end.
@@ -354,9 +354,9 @@ Module Relations.
           {R3 : forall t : base_type, interp_base_type2 t -> interp_base_type3 t -> Prop}
           {t x y z}
     : (forall t a b c, (R1 t a b : Prop) -> (R2 t a c : Prop) -> (R3 t b c : Prop))
-      -> interp_flat_type_rel_pointwise2 (t:=t) R1 x y
-      -> interp_flat_type_rel_pointwise2 (t:=t) R2 x z
-      -> interp_flat_type_rel_pointwise2 (t:=t) R3 y z.
+      -> interp_flat_type_rel_pointwise (t:=t) R1 x y
+      -> interp_flat_type_rel_pointwise (t:=t) R2 x z
+      -> interp_flat_type_rel_pointwise (t:=t) R3 y z.
     Proof.
       intro HRel; induction t; simpl; intuition eauto.
     Qed.
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 900a9f50c..968f83be9 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe25519WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index 4446eb3b6..bcaa5d064 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe2213_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index 1e00f9720..db99360d7 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe2519_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index cf61ffc9c..3d3686a54 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe25519_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index 53a7cb884..b592451eb 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe25519_64WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index 0d803240d..d537c6018 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe41417_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index bd67792af..2ea85da7f 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -509,7 +509,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe5211_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros