Switch to fully uncurried form for reflection

This will eventually make a number of proofs easier.

Unfortunately, the correctness lemmas for AddCoordinates and LadderStep
no longer work (because of different arities), and there's a proof in
Experiments/Ed25519 that I've admitted.

The correctness lemmas will be easy to re-add when we have a more
general version that handle arbitrary type shapes.

1 files changed, 132 insertions, 243 deletions

diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
index 3a95bcc51..2e05b18de 100644
--- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
@@ -1,9 +1,9 @@
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.Classes.RelationClasses.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.Z.InterpretationsGen.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Z.Interpretations64.Relations.
@@ -14,36 +14,6 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.
 
 Module Relations.
-  Section lift.
-    Context {interp_base_type1 interp_base_type2 : base_type -> Type}
-            (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop).
-
-    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_pointwise (t:=T) R f g
-         | Arrow A B
-           => fun f g
-              => 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
-          {t f g}
-      : interp_type_rel_pointwise2 (t:=t) R f g
-        <-> interp_type_rel_pointwise2_uncurried (t:=t) f g.
-    Proof.
-      unfold interp_type_rel_pointwise2_uncurried.
-      induction t as [|A B IHt]; [ reflexivity | ].
-      { simpl; unfold Morphisms.respectful_hetero in *; destruct B.
-        { reflexivity. }
-        { setoid_rewrite IHt; clear IHt.
-          split; intro H; intros.
-          { destruct_head_hnf' prod; simpl in *; intuition. }
-          { eapply (H (_, _) (_, _)); simpl in *; intuition. } } }
-    Qed.
-  End lift.
-
   Section proj.
     Context {interp_base_type1 interp_base_type2}
             (proj : forall t : base_type, interp_base_type1 t -> interp_base_type2 t).
@@ -51,43 +21,27 @@ Module Relations.
     Let R {t : flat_type base_type} f g :=
       SmartVarfMap (t:=t) proj f = g.
 
-    Definition interp_type_rel_pointwise2_uncurried_proj
+    Definition interp_type_rel_pointwise_uncurried_proj
                {t : type base_type}
       : interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop
-      := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop  with
-         | Tflat T => @R _
-         | Arrow A B
-           => fun f g
-              => forall x : interp_flat_type interp_base_type1 (all_binders_for (Arrow A B)),
-                  let y := SmartVarfMap proj x in
-                  let fx := ApplyInterpedAll f x in
-                  let gy := ApplyInterpedAll g y in
-                  @R _ fx gy
-         end.
-
-    Lemma uncurry_interp_type_rel_pointwise2_proj
+      := fun f g
+         => forall x : interp_flat_type interp_base_type1 (domain t),
+             let y := SmartVarfMap proj x in
+             let fx := f x in
+             let gy := g y in
+             @R _ fx gy.
+
+    Lemma uncurry_interp_type_rel_pointwise_proj
           {t : type base_type}
-          {f : interp_type interp_base_type1 t}
+          {f}
           {g}
-      : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g
-        -> interp_type_rel_pointwise2_uncurried_proj (t:=t) f g.
+      : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y))
+        -> interp_type_rel_pointwise_uncurried_proj (t:=t) f g.
     Proof.
-      unfold interp_type_rel_pointwise2_uncurried_proj.
-      induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *.
-      { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit;
-          [ solve [ trivial | reflexivity ] | reflexivity | ].
-        intros [HA HB].
-        specialize (IHA _ _ HA); specialize (IHB _ _ HB).
-        unfold R in *.
-        repeat first [ progress destruct_head_hnf' prod
-                     | progress simpl in *
-                     | progress subst
-                     | reflexivity ]. }
-      { destruct B; intros H ?; apply IHt, H; clear IHt;
-          repeat first [ reflexivity
-                       | progress simpl in *
-                       | progress unfold R, LiftOption.of' in *
-                       | progress break_match ]. }
+      unfold interp_type_rel_pointwise_uncurried_proj.
+      destruct t as [A B]; simpl in *.
+      subst R; simpl in *.
+      eauto.
     Qed.
   End proj.
 
@@ -102,49 +56,28 @@ Module Relations.
       | None => True
       end.
 
-    Definition interp_type_rel_pointwise2_uncurried_proj_option
+    Definition interp_type_rel_pointwise_uncurried_proj_option
                {t : type base_type}
       : interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop
-      := match t return interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop  with
-         | Tflat T => @R _
-         | Arrow A B
-           => fun f g
-              => forall x : interp_flat_type (fun _ => interp_base_type1) (all_binders_for (Arrow A B)),
-                  let y := SmartVarfMap proj_option x in
-                  let fx := ApplyInterpedAll f (LiftOption.to' (Some x)) in
-                  let gy := ApplyInterpedAll g y in
-                  @R _ fx gy
-         end.
-
-    Lemma uncurry_interp_type_rel_pointwise2_proj_option
+      := fun f g
+         => forall x : interp_flat_type (fun _ => interp_base_type1) (domain t),
+             let y := SmartVarfMap proj_option x in
+             let fx := f (LiftOption.to' (Some x)) in
+             let gy := g y in
+             @R _ fx gy.
+
+    Lemma uncurry_interp_type_rel_pointwise_proj_option
           {t : type base_type}
-          {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t}
+          {f}
           {g}
-      : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g
-        -> interp_type_rel_pointwise2_uncurried_proj_option (t:=t) f g.
+      : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y))
+        -> interp_type_rel_pointwise_uncurried_proj_option (t:=t) f g.
     Proof.
-      unfold interp_type_rel_pointwise2_uncurried_proj_option.
-      induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *.
-      { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit;
-          [ solve [ trivial | reflexivity ] | reflexivity | ].
-        intros [HA HB].
-        specialize (IHA _ _ HA); specialize (IHB _ _ HB).
-        unfold R in *.
-        repeat first [ progress destruct_head_hnf' prod
-                     | progress simpl in *
-                     | progress unfold LiftOption.of' in *
-                     | progress break_match
-                     | progress break_match_hyps
-                     | progress inversion_prod
-                     | progress inversion_option
-                     | reflexivity
-                     | progress intuition subst ]. }
-      { destruct B; intros H ?; apply IHt, H; clear IHt.
-        { repeat first [ progress simpl in *
-                       | progress unfold R, LiftOption.of' in *
-                       | progress break_match
-                       | reflexivity ]. }
-        { simpl in *; break_match; reflexivity. } }
+      unfold interp_type_rel_pointwise_uncurried_proj_option.
+      destruct t as [A B]; simpl in *.
+      subst R; simpl in *.
+      intros H x; apply H; simpl.
+      rewrite LiftOption.of'_to'; reflexivity.
     Qed.
   End proj_option.
 
@@ -162,52 +95,58 @@ Module Relations.
       | None, _ => False
       end.
 
-    Definition interp_type_rel_pointwise2_uncurried_proj_option2
+    Definition interp_type_rel_pointwise_uncurried_proj_option2
                {t : type base_type}
       : interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type (LiftOption.interp_base_type' interp_base_type2) t -> Prop
-      := match t return interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type (LiftOption.interp_base_type' interp_base_type2) t -> Prop  with
-         | Tflat T => @R _
-         | Arrow A B
-           => fun f g
-              => forall x : interp_flat_type (fun _ => interp_base_type1) (all_binders_for (Arrow A B)),
-                  let y := SmartVarfMap (fun _ => proj) x in
-                  let fx := ApplyInterpedAll f (LiftOption.to' (Some x)) in
-                  let gy := ApplyInterpedAll g (LiftOption.to' (Some y)) in
-                  @R _ fx gy
-         end.
-
-    Lemma uncurry_interp_type_rel_pointwise2_proj_option2
+      := fun f g
+         => forall x : interp_flat_type (fun _ => interp_base_type1) (domain t),
+             let y := SmartVarfMap (fun _ => proj) x in
+             let fx := f (LiftOption.to' (Some x)) in
+             let gy := g (LiftOption.to' (Some y)) in
+             @R _ fx gy.
+
+    Lemma uncurry_interp_type_rel_pointwise_proj_option2
           {t : type base_type}
-          {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t}
-          {g : interp_type (LiftOption.interp_base_type' interp_base_type2) t}
-      : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g
-        -> interp_type_rel_pointwise2_uncurried_proj_option2 (t:=t) f g.
+          {f}
+          {g}
+      : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y))
+        -> interp_type_rel_pointwise_uncurried_proj_option2 (t:=t) f g.
     Proof.
-      unfold interp_type_rel_pointwise2_uncurried_proj_option2.
-      induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *.
-      { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit;
-          [ solve [ trivial | reflexivity ] | reflexivity | ].
-        intros [HA HB].
-        specialize (IHA _ _ HA); specialize (IHB _ _ HB).
-        unfold R in *.
-        repeat first [ progress destruct_head_hnf' prod
-                     | progress simpl in *
-                     | progress unfold LiftOption.of' in *
-                     | progress break_match
-                     | progress break_match_hyps
-                     | progress inversion_prod
-                     | progress inversion_option
-                     | reflexivity
-                     | progress intuition subst ]. }
-      { destruct B; intros H ?; apply IHt, H; clear IHt.
-        { repeat first [ progress simpl in *
-                       | progress unfold R, LiftOption.of' in *
-                       | progress break_match
-                       | reflexivity ]. }
-        { simpl in *; break_match; reflexivity. } }
+      unfold interp_type_rel_pointwise_uncurried_proj_option2.
+      destruct t as [A B]; simpl in *.
+      subst R; simpl in *.
+      intros H x; apply H; simpl.
+      rewrite !LiftOption.of'_to'; reflexivity.
     Qed.
   End proj_option2.
 
+  Local Ltac t proj012 :=
+    repeat match goal with
+           | _ => progress cbv beta in *
+           | _ => progress break_match; try tauto; []
+           | _ => progress subst
+           | [ H : _ |- _ ]
+             => first [ rewrite !LiftOption.lift_relation_flat_type_pointwise in H
+                        by (eassumption || rewrite LiftOption.of'_to'; reflexivity)
+                      | rewrite !LiftOption.lift_relation2_flat_type_pointwise in H
+                        by (eassumption || rewrite LiftOption.of'_to'; reflexivity)
+                      | rewrite !@lift_interp_flat_type_rel_pointwise_f_eq_id2 in H
+                      | rewrite !@lift_interp_flat_type_rel_pointwise_f_eq in H ]
+           | _ => progress unfold proj_eq_rel in *
+           | _ => progress specialize_by reflexivity
+           | _ => rewrite SmartVarfMap_compose
+           | _ => setoid_rewrite proj012
+           | [ |- context G[fun x y => ?f x y] ]
+             => let G' := context G[f] in change G'
+           | [ |- context G[fun (_ : ?T) x => ?f x] ]
+             => let G' := context G[fun _ : T => f] in change G'
+           | [ H : context G[fun (_ : ?T) x => ?f x] |- _ ]
+             => let G' := context G[fun _ : T => f] in change G' in H
+           | _ => rewrite_hyp <- !*; []
+           | _ => reflexivity
+           | _ => rewrite interp_flat_type_rel_pointwise_SmartVarfMap
+           end.
+
   Section proj_from_option2.
     Context {interp_base_type0 : Type} {interp_base_type1 interp_base_type2 : base_type -> Type}
             (proj01 : forall t, interp_base_type0 -> interp_base_type1 t)
@@ -217,64 +156,41 @@ Module Relations.
     Let R {t : flat_type base_type} f g :=
       proj_eq_rel (SmartVarfMap proj (t:=t)) f g.
 
-    Definition interp_type_rel_pointwise2_uncurried_proj_from_option2
+    Definition interp_type_rel_pointwise_uncurried_proj_from_option2
                {t : type base_type}
       : interp_type (LiftOption.interp_base_type' interp_base_type0) t -> interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop
-      := match t return interp_type _ t -> interp_type _ t -> interp_type _ t -> Prop  with
-         | Tflat T => fun f0 f g => match LiftOption.of' f0 with
-                                    | Some _ => True
-                                    | None => False
-                                    end -> @R _ f g
-         | Arrow A B
-           => fun f0 f g
-              => forall x : interp_flat_type (fun _ => interp_base_type0) (all_binders_for (Arrow A B)),
-                  let x' := SmartVarfMap proj01 x in
-                  let y' := SmartVarfMap proj x' in
-                  let fx := ApplyInterpedAll f x' in
-                  let gy := ApplyInterpedAll g y' in
-                  let f0x := LiftOption.of' (ApplyInterpedAll f0 (LiftOption.to' (Some x))) in
-                  match f0x with
-                  | Some _ => True
-                  | None => False
-                  end
-                  -> @R _ fx gy
-         end.
-
-    Lemma uncurry_interp_type_rel_pointwise2_proj_from_option2
+      := fun f0 f g
+         => forall x : interp_flat_type (fun _ => interp_base_type0) (domain t),
+             let x' := SmartVarfMap proj01 x in
+             let y' := SmartVarfMap proj x' in
+             let fx := f x' in
+             let gy := g y' in
+             let f0x := LiftOption.of' (f0 (LiftOption.to' (Some x))) in
+             match f0x with
+             | Some _ => True
+             | None => False
+             end
+             -> @R _ fx gy.
+
+    Lemma uncurry_interp_type_rel_pointwise_proj_from_option2
           {t : type base_type}
           {f0}
           {f : interp_type interp_base_type1 t}
           {g : interp_type interp_base_type2 t}
           (proj012 : forall t x, proj t (proj01 t x) = proj02 t x)
-      : interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj01 t))) f0 f
-        -> interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g
-        -> interp_type_rel_pointwise2_uncurried_proj_from_option2 (t:=t) f0 f g.
+      : interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj01 t))) f0 f
+        -> interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g
+        -> interp_type_rel_pointwise_uncurried_proj_from_option2 (t:=t) f0 f g.
     Proof.
-      unfold interp_type_rel_pointwise2_uncurried_proj_from_option2.
-      induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *.
-      { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity.
-        { cbv [LiftOption.lift_relation proj_eq_rel R].
-          break_match; try tauto; intros; subst.
-          apply proj012. }
-        { intros [HA HB] [HA' HB'] Hrel.
-          specialize (IHA _ _ _ HA HA'); specialize (IHB _ _ _ HB HB').
-          unfold R, proj_eq_rel in *.
-          repeat first [ progress destruct_head_hnf' prod
-                       | progress simpl in *
-                       | progress unfold LiftOption.of' in *
-                       | progress break_match
-                       | progress break_match_hyps
-                       | progress inversion_prod
-                       | progress inversion_option
-                       | reflexivity
-                       | progress intuition subst ]. } }
-      { destruct B; intros H0 H1 ?; apply IHt; clear IHt; first [ apply H0 | apply H1 ];
-          repeat first [ progress simpl in *
-                       | progress unfold R, LiftOption.of', proj_eq_rel, LiftOption.lift_relation in *
-                       | break_match; rewrite <- ?proj012; reflexivity ]. }
+      unfold interp_type_rel_pointwise_uncurried_proj_from_option2, Morphisms.respectful_hetero.
+      intros H0 H1 x.
+      specialize (H0 (LiftOption.to' (Some x)) (SmartVarfMap proj01 x)).
+      specialize (H1 (LiftOption.to' (Some x)) (SmartVarfMap proj02 x)).
+      subst R.
+      t proj012.
     Qed.
   End proj_from_option2.
-  Global Arguments uncurry_interp_type_rel_pointwise2_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _.
+  Global Arguments uncurry_interp_type_rel_pointwise_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _.
 
   Section proj1_from_option2.
     Context {interp_base_type0 interp_base_type1 : Type} {interp_base_type2 : base_type -> Type}
@@ -282,70 +198,43 @@ Module Relations.
             (proj02 : forall t, interp_base_type0 -> interp_base_type2 t)
             (R : forall t, interp_base_type1 -> interp_base_type2 t -> Prop).
 
-    Definition interp_type_rel_pointwise2_uncurried_proj1_from_option2
+    Definition interp_type_rel_pointwise_uncurried_proj1_from_option2
                {t : type base_type}
       : interp_type (LiftOption.interp_base_type' interp_base_type0) t -> interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop
-      := match t return interp_type _ t -> interp_type _ t -> interp_type _ t -> Prop  with
-         | Tflat T => fun f0 f g => match LiftOption.of' f0 with
-                                    | Some _ => True
-                                    | None => False
-                                    end -> match LiftOption.of' f with
-                                           | Some f' => interp_flat_type_rel_pointwise (@R) f' g
-                                           | None => True
-                                           end
-         | Arrow A B
-           => fun f0 f g
-              => forall x : interp_flat_type (fun _ => interp_base_type0) (all_binders_for (Arrow A B)),
-                  let x' := SmartVarfMap (fun _ => proj01) x in
-                  let y' := SmartVarfMap proj02 x in
-                  let fx := LiftOption.of' (ApplyInterpedAll f (LiftOption.to' (Some x'))) in
-                  let gy := ApplyInterpedAll g y' in
-                  let f0x := LiftOption.of' (ApplyInterpedAll f0 (LiftOption.to' (Some x))) in
-                  match f0x with
-                  | Some _ => True
-                  | None => False
-                  end
-                  -> match fx with
-                     | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy
-                     | None => True
-                     end
-         end.
-
-    Lemma uncurry_interp_type_rel_pointwise2_proj1_from_option2
+      := fun f0 f g
+         => forall x : interp_flat_type (fun _ => interp_base_type0) (domain t),
+             let x' := SmartVarfMap (fun _ => proj01) x in
+             let y' := SmartVarfMap proj02 x in
+             let fx := LiftOption.of' (f (LiftOption.to' (Some x'))) in
+             let gy := g y' in
+             let f0x := LiftOption.of' (f0 (LiftOption.to' (Some x))) in
+             match f0x with
+             | Some _ => True
+             | None => False
+             end
+             -> match fx with
+                | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy
+                | None => True
+                end.
+
+    Lemma uncurry_interp_type_rel_pointwise_proj1_from_option2
           {t : type base_type}
           {f0}
           {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t}
           {g : interp_type interp_base_type2 t}
-          (proj012R : forall t x, @R _ (proj01 x) (proj02 t x))
-      : interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation2 (proj_eq_rel proj01)) f0 f
-        -> interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g
-        -> interp_type_rel_pointwise2_uncurried_proj1_from_option2 (t:=t) f0 f g.
+          (proj012R : forall t, Reflexive (fun x y => @R _ (proj01 x) (proj02 t y)))
+      : interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation2 (proj_eq_rel proj01)) f0 f
+        -> interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g
+        -> interp_type_rel_pointwise_uncurried_proj1_from_option2 (t:=t) f0 f g.
     Proof.
-      unfold interp_type_rel_pointwise2_uncurried_proj1_from_option2.
-      induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *.
-      { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity.
-        { cbv [LiftOption.lift_relation proj_eq_rel LiftOption.lift_relation2].
-          break_match; try tauto; intros; subst.
-          apply proj012R. }
-        { intros [HA HB] [HA' HB'] Hrel.
-          specialize (IHA _ _ _ HA HA'); specialize (IHB _ _ _ HB HB').
-          unfold proj_eq_rel in *.
-          repeat first [ progress destruct_head_hnf' prod
-                       | progress simpl in *
-                       | progress unfold LiftOption.of' in *
-                       | progress break_match
-                       | progress break_match_hyps
-                       | progress inversion_prod
-                       | progress inversion_option
-                       | reflexivity
-                       | progress intuition subst ]. } }
-      { destruct B; intros H0 H1 ?; apply IHt; clear IHt; first [ apply H0 | apply H1 ];
-          repeat first [ progress simpl in *
-                       | progress unfold R, LiftOption.of', proj_eq_rel, LiftOption.lift_relation in *
-                       | break_match; reflexivity ]. }
+      unfold interp_type_rel_pointwise_uncurried_proj1_from_option2, Morphisms.respectful_hetero.
+      intros H0 H1 x.
+      specialize (H0 (LiftOption.to' (Some x)) (LiftOption.to' (Some (SmartVarfMap (fun _ => proj01) x)))).
+      specialize (H1 (LiftOption.to' (Some x)) (SmartVarfMap proj02 x)).
+      t proj012.
     Qed.
   End proj1_from_option2.
-  Global Arguments uncurry_interp_type_rel_pointwise2_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _.
+  Global Arguments uncurry_interp_type_rel_pointwise_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _.
 
   Section combine_related.
     Lemma related_flat_transitivity {interp_base_type1 interp_base_type2 interp_base_type3}