Adequacy (Def 6.1)

We prove in this module that the composition of strategy is adequate. The proof essentially proceeds by showing that "evaluating and observing", i.e., reduce, is a solution of the same equations as is the composition of strategies.

This argument assumes we can rely on the unicity of such a solution: we prove this fact by proving that these equations are eventually guarded in OGS/CompGuarded.v.

We consider a language abstractly captured as a machine satisfying an appropriate axiomatization.

  Context {T C} {CC : context T C} {CL : context_laws T C}.
  Context {val} {VM : subst_monoid val} {VML : subst_monoid_laws val}.
  Context {conf} {CM : subst_module val conf} {CML : subst_module_laws val conf}.
  Context {obs : obs_struct T C} {M : machine val conf obs} {ML : machine_laws val conf obs}.
  Context {VV : var_assumptions val}.

We define reduce, called "zip-then-eval-then-observe" in the paper.

  Definition reduce {Δ} (x : reduce_t Δ)
    : delay (obs∙ Δ)
    := evalₒ (x.(red_act).(ms_conf)
              ₜ⊛ [ a_id , bicollapse x.(red_act).(ms_env) x.(red_pas) ]) .

  Definition reduce' {Δ} : forall i, reduce_t Δ -> itree ∅ₑ (fun _ : T1 => obs∙ Δ) i
    := fun 'T1_0 => reduce .

Equipped with eventually guarded equations, we are ready to prove the adequacy.

First a technical lemma, rewriting one step of compo, then reduce to a simpler more explicit form.

  Lemma compo_reduce_simpl {Δ} (x : reduce_t Δ) :
    (compo_body x >>= fun _ r =>
         match r with
         | inl y => reduce' _ y
         | inr o => Ret' (o : (fun _ => obs∙ _) _)
         end)
      ≊
      (eval x.(red_act).(ms_conf) >>= fun _ n =>
           match c_view_cat (nf_var n) with
           | Vcat_l i => Ret' (i ⋅ nf_obs n)
           | Vcat_r j => reduce' _ (RedT (m_strat_resp x.(red_pas) (j ⋅ nf_obs n))
                                        (x.(red_act).(ms_env) ;⁻ nf_args n))
           end).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: reduce_t Δ
(compo_body x >>=
 (fun (i : T1)
    (r : (fun _ : T1 => (reduce_t Δ + obs ∙ Δ)%type) i)
  =>
  match r with
  | inl y => reduce' i y
  | inr o => Ret' (o : (fun _ : T1 => obs ∙ Δ) i)
  end))
≊ (eval (ms_conf (red_act x)) >>=
   (fun (i : T1)
      (n : (fun _ : T1 =>
            nf obs val
              (Δ +▶ Game.join_pol Game.Act (red_ctx x)))
             i) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
    | Vcat_r j =>
        reduce' i
          {|
            red_ctx := Game.g_next (j ⋅ nf_obs n);
            red_act :=
              m_strat_resp (red_pas x) (j ⋅ nf_obs n);
            red_pas := ms_env (red_act x);⁻ nf_args n
          |}
    end))
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: reduce_t Δ
(compo_body x >>=
 (fun (i : T1)
    (r : (fun _ : T1 => (reduce_t Δ + obs ∙ Δ)%type) i)
  =>
  match r with
  | inl y => reduce' i y
  | inr o => Ret' (o : (fun _ : T1 => obs ∙ Δ) i)
  end))
≊ (eval (ms_conf (red_act x)) >>=
   (fun (i : T1)
      (n : (fun _ : T1 =>
            nf obs val
              (Δ +▶ Game.join_pol Game.Act (red_ctx x)))
             i) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
    | Vcat_r j =>
        reduce' i
          {|
            red_ctx := Game.g_next (j ⋅ nf_obs n);
            red_act :=
              m_strat_resp (red_pas x) (j ⋅ nf_obs n);
            red_pas := ms_env (red_act x);⁻ nf_args n
          |}
    end))
    do 2 (etransitivity; [ now apply fmap_bind_com | ]).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: reduce_t Δ
(eval (ms_conf (red_act x)) >>=
 (fun i : T1 =>
  (fun (i0 : T1)
     (x1 : obs ∙ Δ +
           {m : Game.g_move (red_ctx x) &
           m_strat_pas Δ (Game.g_next m)}) =>
   match
     match x1 with
     | inl r => inr r
     | inr e =>
         inl
           {|
             red_ctx := Game.g_next (projT1 e);
             red_act :=
               m_strat_resp (red_pas x) (projT1 e);
             red_pas := projT2 e
           |}
     end
   with
   | inl y => reduce' i0 y
   | inr o => Ret' o
   end) i
  ∘ (fun _ : T1 => m_strat_wrap (ms_env (red_act x)))
      i))
≊ (eval (ms_conf (red_act x)) >>=
   (fun (i : T1)
      (n : nf obs val
             (Δ +▶ Game.join_pol Game.Act (red_ctx x)))
    =>
    match c_view_cat (nf_var n) with
    | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
    | Vcat_r j =>
        reduce' i
          {|
            red_ctx := Game.g_next (j ⋅ nf_obs n);
            red_act :=
              m_strat_resp (red_pas x) (j ⋅ nf_obs n);
            red_pas := ms_env (red_act x);⁻ nf_args n
          |}
    end))
    apply (subst_eq (RX := fun _ => eq)); eauto.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: reduce_t Δ
dpointwise_relation
  (fun i : T1 =>
   (eq ==> it_eq (eqᵢ (fun _ : T1 => obs ∙ Δ)) (i:=i))%signature)
  (fun (i : T1)
     (x0 : nf obs val
             (Δ +▶ Game.join_pol Game.Act (red_ctx x)))
   =>
   match
     match m_strat_wrap (ms_env (red_act x)) x0 with
     | inl r => inr r
     | inr e =>
         inl
           {|
             red_ctx := Game.g_next (projT1 e);
             red_act :=
               m_strat_resp (red_pas x) (projT1 e);
             red_pas := projT2 e
           |}
     end
   with
   | inl y => reduce' i y
   | inr o => Ret' o
   end)
  (fun (i : T1)
     (n : nf obs val
            (Δ +▶ Game.join_pol Game.Act (red_ctx x)))
   =>
   match c_view_cat (nf_var n) with
   | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
   | Vcat_r j =>
       reduce' i
         {|
           red_ctx := Game.g_next (j ⋅ nf_obs n);
           red_act :=
             m_strat_resp (red_pas x) (j ⋅ nf_obs n);
           red_pas := ms_env (red_act x);⁻ nf_args n
         |}
   end)
    intros ? [ ? i [ ? ? ] ] ? <-.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: reduce_t Δ
a: T1
cut_ty: T
i: Δ +▶ Game.join_pol Game.Act (red_ctx x) ∋ cut_ty
fill_op: obs cut_ty
fill_args: dom fill_op =[ val
]> (Δ +▶
    Game.join_pol Game.Act (red_ctx x))
match
  match
    m_strat_wrap (ms_env (red_act x))
      (i ⋅ fill_op ⦇ fill_args ⦈)
  with
  | inl r => inr r
  | inr e =>
      inl
        {|
          red_ctx := Game.g_next (projT1 e);
          red_act :=
            m_strat_resp (red_pas x) (projT1 e);
          red_pas := projT2 e
        |}
  end
with
| inl y => reduce' a y
| inr o => Ret' o
end
≊ match
    c_view_cat (nf_var (i ⋅ fill_op ⦇ fill_args ⦈))
  with
  | Vcat_l i0 =>
      Ret' (i0 ⋅ nf_obs (i ⋅ fill_op ⦇ fill_args ⦈))
  | Vcat_r j =>
      reduce' a
        {|
          red_ctx :=
            Game.g_next
              (j ⋅ nf_obs (i ⋅ fill_op ⦇ fill_args ⦈));
          red_act :=
            m_strat_resp 
              (red_pas x)
              (j ⋅ nf_obs (i ⋅ fill_op ⦇ fill_args ⦈));
          red_pas :=
            ms_env (red_act x);⁻
            nf_args (i ⋅ fill_op ⦇ fill_args ⦈)
        |}
  end
    unfold m_strat_wrap; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
x: reduce_t Δ
a: T1
cut_ty: T
i: Δ +▶ Game.join_pol Game.Act (red_ctx x) ∋ cut_ty
fill_op: obs cut_ty
fill_args: dom fill_op =[ val
]> (Δ +▶
    Game.join_pol Game.Act (red_ctx x))
match
  match
    match c_view_cat i with
    | Vcat_l i => inl (i ⋅ fill_op)
    | Vcat_r j =>
        inr
          ((j ⋅ fill_op),'
           (ms_env (red_act x);⁻
            nf_args (i ⋅ fill_op ⦇ fill_args ⦈)))
    end
  with
  | inl r => inr r
  | inr e =>
      inl
        {|
          red_ctx := red_ctx x ▶ₓ m_dom (projT1 e);
          red_act :=
            m_strat_resp (red_pas x) (projT1 e);
          red_pas := projT2 e
        |}
  end
with
| inl y => reduce' a y
| inr o => Ret' o
end
≊ match c_view_cat i with
  | Vcat_l i => Ret' (i ⋅ fill_op)
  | Vcat_r j =>
      reduce' a
        {|
          red_ctx := red_ctx x ▶ₓ dom fill_op;
          red_act :=
            m_strat_resp (red_pas x) (j ⋅ fill_op);
          red_pas :=
            ms_env (red_act x);⁻
            nf_args (i ⋅ fill_op ⦇ fill_args ⦈)
        |}
  end
    now destruct (c_view_cat i).
  Qed.

Next we derive a variant of "evaluation respects substitution", working with partial assignments [ a_id , e ] instead of full assignments.

  Definition eval_split_sub {Γ Δ} (c : conf (Δ +▶ Γ)) (e : Γ =[val]> Δ)
    : delay (nf obs val Δ)
    := eval c >>= fun 'T1_0 n =>
         match c_view_cat (nf_var n) with
         | Vcat_l i => Ret' (i ⋅ nf_obs n ⦇ nf_args n ⊛ [ v_var,  e ] ⦈)
         | Vcat_r j => eval (e _ j ⊙ nf_obs n ⦗ nf_args n ⊛ [ v_var,  e ] ⦘)
         end .

  Lemma eval_split {Γ Δ} (c : conf (Δ +▶ Γ)) (e : Γ =[val]> Δ) :
    eval (c ₜ⊛ [ a_id , e ]) ≋ eval_split_sub c e .
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
eval (c ₜ⊛ [a_id, e]) ≋ eval_split_sub c e
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
eval (c ₜ⊛ [a_id, e]) ≋ eval_split_sub c e
    unfold eval_split_sub.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
eval (c ₜ⊛ [a_id, e])
≋ eval c >>=
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (nf obs val (Δ +▶ Γ) ->
       itree ∅ₑ (fun _ : T1 => nf obs val Δ) x) in
    fun n : nf obs val (Δ +▶ Γ) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i =>
        Ret' (i ⋅ nf_obs n ⦇ nf_args n ⊛ [a_id, e] ⦈)
    | Vcat_r j =>
        eval
          (e (nf_ty n) j ⊙ 
           nf_obs n ⦗ nf_args n ⊛ [a_id, e] ⦘)
    end)
    rewrite (eval_sub c ([ v_var , e ])).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
bind_delay' (eval c)
  (fun n : nf obs val (Δ +▶ Γ) =>
   eval (emb n ₜ⊛ [a_id, e]))
≋ eval c >>=
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (nf obs val (Δ +▶ Γ) ->
       itree ∅ₑ (fun _ : T1 => nf obs val Δ) x) in
    fun n : nf obs val (Δ +▶ Γ) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i =>
        Ret' (i ⋅ nf_obs n ⦇ nf_args n ⊛ [a_id, e] ⦈)
    | Vcat_r j =>
        eval
          (e (nf_ty n) j ⊙ 
           nf_obs n ⦗ nf_args n ⊛ [a_id, e] ⦘)
    end)
    apply (subst_eq (RX := fun _ => eq)); eauto.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
dpointwise_relation
  (fun i : T1 =>
   (eq ==> it_eq (fun _ : T1 => nf_eq) (i:=i))%signature)
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (nf obs val (Δ +▶ Γ) ->
       itree ∅ₑ (fun _ : T1 => nf obs val Δ) x) in
    fun y : nf obs val (Δ +▶ Γ) =>
    eval (emb y ₜ⊛ [a_id, e]))
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (nf obs val (Δ +▶ Γ) ->
       itree ∅ₑ (fun _ : T1 => nf obs val Δ) x) in
    fun n : nf obs val (Δ +▶ Γ) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i =>
        Ret' (i ⋅ nf_obs n ⦇ nf_args n ⊛ [a_id, e] ⦈)
    | Vcat_r j =>
        eval
          (e (nf_ty n) j ⊙ 
           nf_obs n ⦗ nf_args n ⊛ [a_id, e] ⦘)
    end)
    intros [] [ ? i [ o a ] ] ? <-; unfold emb; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
i: Δ +▶ Γ ∋ cut_ty
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
it_eq (fun _ : T1 => nf_eq)
  (eval
     (a_id i ⊙ o ⦗ nf_args (i ⋅ o ⦇ a ⦈) ⦘
      ₜ⊛ [a_id, e]))
  match c_view_cat i with
  | Vcat_l i0 =>
      Ret'
        (i0 ⋅ o ⦇ nf_args (i ⋅ o ⦇ a ⦈) ⊛ [a_id, e] ⦈)
  | Vcat_r j =>
      eval
        (e cut_ty j ⊙ o
         ⦗ nf_args (i ⋅ o ⦇ a ⦈) ⊛ [a_id, e] ⦘)
  end
    destruct (c_view_cat i).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
i: Δ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval
     (a_id (r_cat_l i) ⊙ o
      ⦗ nf_args (r_cat_l i ⋅ o ⦇ a ⦈) ⦘ ₜ⊛ 
      [a_id, e]))
  (Ret'
     (i
      ⋅ o ⦇ nf_args (r_cat_l i ⋅ o ⦇ a ⦈) ⊛ [a_id, e]
        ⦈))
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
j: Γ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval
     (a_id (r_cat_r j) ⊙ o
      ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈) ⦘ ₜ⊛ 
      [a_id, e]))
  (eval
     (e cut_ty j ⊙ o
      ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈) ⊛ [a_id, e] ⦘))
    +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
i: Δ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval
     (a_id (r_cat_l i) ⊙ o
      ⦗ nf_args (r_cat_l i ⋅ o ⦇ a ⦈) ⦘ ₜ⊛ 
      [a_id, e]))
  (Ret'
     (i
      ⋅ o ⦇ nf_args (r_cat_l i ⋅ o ⦇ a ⦈) ⊛ [a_id, e]
        ⦈)) unfold nf_args, fill_args, cut_r.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
i: Δ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval (a_id (r_cat_l i) ⊙ o ⦗ a ⦘ ₜ⊛ [a_id, e]))
  (Ret' (i ⋅ o ⦇ a ⊛ [a_id, e] ⦈))
      rewrite app_sub, v_sub_var.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
i: Δ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval
     (([a_id, e])%asgn cut_ty (r_cat_l i) ⊙ o
      ⦗ a ⊛ [a_id, e] ⦘))
  (Ret' (i ⋅ o ⦇ a ⊛ [a_id, e] ⦈))
      cbn; rewrite c_view_cat_simpl_l.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
i: Δ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval (a_id i ⊙ o ⦗ a ⊛ [a_id, e] ⦘))
  (Ret' (i ⋅ o ⦇ a ⊛ [a_id, e] ⦈))
      now apply (eval_nf_ret (i ⋅ o ⦇ a ⊛ [a_id, e] ⦈)).
    +
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
j: Γ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval
     (a_id (r_cat_r j) ⊙ o
      ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈) ⦘ ₜ⊛ 
      [a_id, e]))
  (eval
     (e cut_ty j ⊙ o
      ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈) ⊛ [a_id, e] ⦘)) rewrite app_sub, v_sub_var.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
c: conf (Δ +▶ Γ)
e: Γ =[ val ]> Δ
cut_ty: T
o: obs cut_ty
a: dom o =[ val ]> (Δ +▶ Γ)
j: Γ ∋ cut_ty
it_eq (fun _ : T1 => nf_eq)
  (eval
     (([a_id, e])%asgn cut_ty (r_cat_r j) ⊙ o
      ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈) ⊛ [a_id, e] ⦘))
  (eval
     (e cut_ty j ⊙ o
      ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈) ⊛ [a_id, e] ⦘))
      cbn; now rewrite c_view_cat_simpl_r.
  Qed.

Note the use of iter_evg_uniq: the proof of adequacy is proved by unicity of the fixed point, which is made possible by equivalently viewing the fixpoint combinator used to define the composition of strategy as a fixpoint of eventually guarded equations.

  Lemma adequacy_gen {Δ a} (c : m_strat_act Δ a) (e : m_strat_pas Δ a) :
    reduce (RedT c e) ≊ (c ∥g e).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
a: Game.ogs_ctx
c: m_strat_act Δ a
e: m_strat_pas Δ a
reduce {| red_ctx := a; red_act := c; red_pas := e |}
≊ (c ∥g e)
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
a: Game.ogs_ctx
c: m_strat_act Δ a
e: m_strat_pas Δ a
reduce {| red_ctx := a; red_act := c; red_pas := e |}
≊ (c ∥g e)
    refine (iter_evg_uniq (fun 'T1_0 u => compo_body u) (fun 'T1_0 u => reduce u) _ _ T1_0 _).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
a: Game.ogs_ctx
c: m_strat_act Δ a
e: m_strat_pas Δ a
forall (i : T1) (x : reduce_t Δ),
(let
 'T1_0 as x0 := i
  return
    (reduce_t Δ -> itree ∅ₑ (fun _ : T1 => obs ∙ Δ) x0)
  in fun u : reduce_t Δ => reduce u) x
≊ ((let
    'T1_0 as x0 := i
     return
       (reduce_t Δ ->
        itree ∅ₑ
          ((fun _ : T1 => reduce_t Δ) +ᵢ
           (fun _ : T1 => obs ∙ Δ)) x0) in
     fun u : reduce_t Δ => compo_body u) x >>=
   (fun (i0 : T1)
      (r : ((fun _ : T1 => reduce_t Δ) +ᵢ
            (fun _ : T1 => obs ∙ Δ)) i0) =>
    match r with
    | inl x0 =>
        (let
         'T1_0 as x1 := i0
          return
            (reduce_t Δ ->
             itree ∅ₑ (fun _ : T1 => obs ∙ Δ) x1) in
          fun u : reduce_t Δ => reduce u) x0
    | inr y => Ret' y
    end))
    clear a c e; intros [] [ ? [ u v ] ].
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
reduce
  {|
    red_ctx := red_ctx;
    red_act := {| ms_conf := u; ms_env := v |};
    red_pas := red_pas
  |}
≊ (compo_body
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |} >>=
   (fun (i : T1)
      (r : ((fun _ : T1 => reduce_t Δ) +ᵢ
            (fun _ : T1 => obs ∙ Δ)) i) =>
    match r with
    | inl x =>
        (let
         'T1_0 as x0 := i
          return
            (reduce_t Δ ->
             itree ∅ₑ (fun _ : T1 => obs ∙ Δ) x0) in
          fun u : reduce_t Δ => reduce u) x
    | inr y => Ret' y
    end))
    etransitivity; [ | symmetry; apply compo_reduce_simpl ].
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
reduce
  {|
    red_ctx := red_ctx;
    red_act := {| ms_conf := u; ms_env := v |};
    red_pas := red_pas
  |}
≊ (eval
     (ms_conf
        (red_act
           {|
             red_ctx := red_ctx;
             red_act :=
               {| ms_conf := u; ms_env := v |};
             red_pas := red_pas
           |})) >>=
   (fun (i : T1)
      (n : nf obs val
             (Δ +▶
              Game.join_pol Game.Act
                (Strategy.red_ctx
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |}))) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
    | Vcat_r j =>
        reduce' i
          {|
            red_ctx := Game.g_next (j ⋅ nf_obs n);
            red_act :=
              m_strat_resp
                (Strategy.red_pas
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |}) (j ⋅ nf_obs n);
            red_pas :=
              ms_env
                (red_act
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |});⁻ 
              nf_args n
          |}
    end))
    unfold reduce at 1, evalₒ at 1; rewrite eval_split.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
then_to_obs
  (eval_split_sub
     (ms_conf
        (red_act
           {|
             red_ctx := red_ctx;
             red_act :=
               {| ms_conf := u; ms_env := v |};
             red_pas := red_pas
           |}))
     (bicollapse
        (ms_env
           (red_act
              {|
                red_ctx := red_ctx;
                red_act :=
                  {| ms_conf := u; ms_env := v |};
                red_pas := red_pas
              |}))
        (Strategy.red_pas
           {|
             red_ctx := red_ctx;
             red_act :=
               {| ms_conf := u; ms_env := v |};
             red_pas := red_pas
           |})))
≊ (eval
     (ms_conf
        (red_act
           {|
             red_ctx := red_ctx;
             red_act :=
               {| ms_conf := u; ms_env := v |};
             red_pas := red_pas
           |})) >>=
   (fun (i : T1)
      (n : nf obs val
             (Δ +▶
              Game.join_pol Game.Act
                (Strategy.red_ctx
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |}))) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
    | Vcat_r j =>
        reduce' i
          {|
            red_ctx := Game.g_next (j ⋅ nf_obs n);
            red_act :=
              m_strat_resp
                (Strategy.red_pas
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |}) (j ⋅ nf_obs n);
            red_pas :=
              ms_env
                (red_act
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |});⁻ 
              nf_args n
          |}
    end))
    etransitivity; [ apply bind_fmap_com | ].
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
(eval
   (ms_conf
      (red_act
         {|
           red_ctx := red_ctx;
           red_act := {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |})) >>=
 (fun i : T1 =>
  fmap (fun _ : T1 => nf_to_obs Δ) i
  ∘ (fun pat : T1 =>
     let
     'T1_0 as x0 := pat
      return
        (nf obs val
           (Δ +▶
            Game.join_pol Game.Act
              (Strategy.red_ctx
                 {|
                   red_ctx := red_ctx;
                   red_act :=
                     {| ms_conf := u; ms_env := v |};
                   red_pas := red_pas
                 |})) ->
         itree ∅ₑ (fun _ : T1 => nf obs val Δ) x0) in
      fun
        n : nf obs val
              (Δ +▶
               Game.join_pol Game.Act
                 (Strategy.red_ctx
                    {|
                      red_ctx := red_ctx;
                      red_act :=
                        {|
                        ms_conf := u; ms_env := v
                        |};
                      red_pas := red_pas
                    |})) =>
      match c_view_cat (nf_var n) with
      | Vcat_l i0 =>
          Ret'
            (i0
             ⋅ nf_obs n
               ⦇ nf_args n
                 ⊛ [a_id,
                   bicollapse
                     (ms_env
                        (red_act {| ...; ...; ... |}))
                     (Strategy.red_pas
                        {|
                        red_ctx := red_ctx;
                        red_act := {| ... |};
                        red_pas := red_pas
                        |})] ⦈)
      | Vcat_r j =>
          eval
            (bicollapse
               (ms_env
                  (red_act
                     {|
                       red_ctx := red_ctx;
                       red_act := {| ...; ... |};
                       red_pas := red_pas
                     |}))
               (Strategy.red_pas
                  {|
                    red_ctx := red_ctx;
                    red_act :=
                      {| ms_conf := u; ms_env := v |};
                    red_pas := red_pas
                  |}) (nf_ty n) j ⊙ 
             nf_obs n
             ⦗ nf_args n
               ⊛ [a_id,
                 bicollapse
                   (ms_env
                      (red_act
                        {|
                        red_ctx := red_ctx;
                        red_act := ...;
                        red_pas := red_pas
                        |}))
                   (Strategy.red_pas
                      {|
                        red_ctx := red_ctx;
                        red_act := {| ...; ... |};
                        red_pas := red_pas
                      |})] ⦘)
      end) i))
≊ (eval
     (ms_conf
        (red_act
           {|
             red_ctx := red_ctx;
             red_act :=
               {| ms_conf := u; ms_env := v |};
             red_pas := red_pas
           |})) >>=
   (fun (i : T1)
      (n : nf obs val
             (Δ +▶
              Game.join_pol Game.Act
                (Strategy.red_ctx
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |}))) =>
    match c_view_cat (nf_var n) with
    | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
    | Vcat_r j =>
        reduce' i
          {|
            red_ctx := Game.g_next (j ⋅ nf_obs n);
            red_act :=
              m_strat_resp
                (Strategy.red_pas
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |}) (j ⋅ nf_obs n);
            red_pas :=
              ms_env
                (red_act
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |});⁻ 
              nf_args n
          |}
    end))
    apply (subst_eq (RX := fun _ => eq)); eauto.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
dpointwise_relation
  (fun i : T1 =>
   (eq ==> it_eq (eqᵢ (fun _ : T1 => obs ∙ Δ)) (i:=i))%signature)
  (fun i : T1 =>
   fmap (fun _ : T1 => nf_to_obs Δ) i
   ∘ (let
      'T1_0 as x0 := i
       return
         (nf obs val
            (Δ +▶
             Game.join_pol Game.Act
               (Strategy.red_ctx
                  {|
                    red_ctx := red_ctx;
                    red_act :=
                      {| ms_conf := u; ms_env := v |};
                    red_pas := red_pas
                  |})) ->
          itree ∅ₑ (fun _ : T1 => nf obs val Δ) x0) in
       fun
         n : nf obs val
               (Δ +▶
                Game.join_pol Game.Act
                  (Strategy.red_ctx
                     {|
                       red_ctx := red_ctx;
                       red_act :=
                        {|
                        ms_conf := u; ms_env := v
                        |};
                       red_pas := red_pas
                     |})) =>
       match c_view_cat (nf_var n) with
       | Vcat_l i0 =>
           Ret'
             (i0
              ⋅ nf_obs n
                ⦇ nf_args n
                  ⊛ [a_id,
                    bicollapse
                      (ms_env
                        (red_act
                        {|
                        red_ctx := red_ctx;
                        red_act :=
                        {|
                        ms_conf := u; ms_env := v
                        |};
                        red_pas := red_pas
                        |}))
                      (Strategy.red_pas
                        {|
                        red_ctx := red_ctx;
                        red_act :=
                        {|
                        ms_conf := u; ms_env := v
                        |};
                        red_pas := red_pas
                        |})] ⦈)
       | Vcat_r j =>
           eval
             (bicollapse
                (ms_env
                   (red_act
                      {|
                        red_ctx := red_ctx;
                        red_act :=
                        {|
                        ms_conf := u; ms_env := v
                        |};
                        red_pas := red_pas
                      |}))
                (Strategy.red_pas
                   {|
                     red_ctx := red_ctx;
                     red_act :=
                       {| ms_conf := u; ms_env := v |};
                     red_pas := red_pas
                   |}) (nf_ty n) j ⊙ 
              nf_obs n
              ⦗ nf_args n
                ⊛ [a_id,
                  bicollapse
                    (ms_env
                       (red_act
                        {|
                        red_ctx := red_ctx;
                        red_act :=
                        {|
                        ms_conf := u; ms_env := v
                        |};
                        red_pas := red_pas
                        |}))
                    (Strategy.red_pas
                       {|
                        red_ctx := red_ctx;
                        red_act :=
                        {|
                        ms_conf := u; ms_env := v
                        |};
                        red_pas := red_pas
                       |})] ⦘)
       end))
  (fun (i : T1)
     (n : nf obs val
            (Δ +▶
             Game.join_pol Game.Act
               (Strategy.red_ctx
                  {|
                    red_ctx := red_ctx;
                    red_act :=
                      {| ms_conf := u; ms_env := v |};
                    red_pas := red_pas
                  |}))) =>
   match c_view_cat (nf_var n) with
   | Vcat_l i0 => Ret' (i0 ⋅ nf_obs n)
   | Vcat_r j =>
       reduce' i
         {|
           red_ctx := Game.g_next (j ⋅ nf_obs n);
           red_act :=
             m_strat_resp
               (Strategy.red_pas
                  {|
                    red_ctx := red_ctx;
                    red_act :=
                      {| ms_conf := u; ms_env := v |};
                    red_pas := red_pas
                  |}) (j ⋅ nf_obs n);
           red_pas :=
             ms_env
               (red_act
                  {|
                    red_ctx := red_ctx;
                    red_act :=
                      {| ms_conf := u; ms_env := v |};
                    red_pas := red_pas
                  |});⁻ nf_args n
         |}
   end)
    intros [] [ ? i [ o a ] ] ? <-; unfold emb; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
i: Δ +▶
Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
((fun _ : T1 => nf_to_obs Δ) <$>
 match c_view_cat i with
 | Vcat_l i0 =>
     Ret'
       (i0
        ⋅ o
          ⦇ nf_args (i ⋅ o ⦇ a ⦈)
            ⊛ [a_id, bicollapse v red_pas] ⦈)
 | Vcat_r j =>
     eval
       (bicollapse v red_pas cut_ty j ⊙ o
        ⦗ nf_args (i ⋅ o ⦇ a ⦈)
          ⊛ [a_id, bicollapse v red_pas] ⦘)
 end)
≊ match c_view_cat i with
  | Vcat_l i => Ret' (i ⋅ o)
  | Vcat_r j =>
      reduce
        {|
          red_ctx := red_ctx ▶ₓ dom o;
          red_act := m_strat_resp red_pas (j ⋅ o);
          red_pas := v;⁻ nf_args (i ⋅ o ⦇ a ⦈)
        |}
  end
    destruct (c_view_cat i).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
i: Δ ∋ cut_ty
((fun _ : T1 => nf_to_obs Δ) <$>
 match c_view_cat (r_cat_l i) with
 | Vcat_l i0 =>
     Ret'
       (i0
        ⋅ o
          ⦇ nf_args (r_cat_l i ⋅ o ⦇ a ⦈)
            ⊛ [a_id, bicollapse v red_pas] ⦈)
 | Vcat_r j =>
     eval
       (bicollapse v red_pas cut_ty j ⊙ o
        ⦗ nf_args (r_cat_l i ⋅ o ⦇ a ⦈)
          ⊛ [a_id, bicollapse v red_pas] ⦘)
 end)
≊ match c_view_cat (r_cat_l i) with
  | Vcat_l i => Ret' (i ⋅ o)
  | Vcat_r j =>
      reduce
        {|
          red_ctx := red_ctx ▶ₓ dom o;
          red_act := m_strat_resp red_pas (j ⋅ o);
          red_pas := v;⁻ nf_args (r_cat_l i ⋅ o ⦇ a ⦈)
        |}
  end
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
((fun _ : T1 => nf_to_obs Δ) <$>
 match c_view_cat (r_cat_r j) with
 | Vcat_l i =>
     Ret'
       (i
        ⋅ o
          ⦇ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
            ⊛ [a_id, bicollapse v red_pas] ⦈)
 | Vcat_r j0 =>
     eval
       (bicollapse v red_pas cut_ty j0 ⊙ o
        ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
          ⊛ [a_id, bicollapse v red_pas] ⦘)
 end)
≊ match c_view_cat (r_cat_r j) with
  | Vcat_l i => Ret' (i ⋅ o)
  | Vcat_r j0 =>
      reduce
        {|
          red_ctx := red_ctx ▶ₓ dom o;
          red_act := m_strat_resp red_pas (j0 ⋅ o);
          red_pas := v;⁻ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
        |}
  end
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
i: Δ ∋ cut_ty
((fun _ : T1 => nf_to_obs Δ) <$>
 match c_view_cat (r_cat_l i) with
 | Vcat_l i0 =>
     Ret'
       (i0
        ⋅ o
          ⦇ nf_args (r_cat_l i ⋅ o ⦇ a ⦈)
            ⊛ [a_id, bicollapse v red_pas] ⦈)
 | Vcat_r j =>
     eval
       (bicollapse v red_pas cut_ty j ⊙ o
        ⦗ nf_args (r_cat_l i ⋅ o ⦇ a ⦈)
          ⊛ [a_id, bicollapse v red_pas] ⦘)
 end)
≊ match c_view_cat (r_cat_l i) with
  | Vcat_l i => Ret' (i ⋅ o)
  | Vcat_r j =>
      reduce
        {|
          red_ctx := red_ctx ▶ₓ dom o;
          red_act := m_strat_resp red_pas (j ⋅ o);
          red_pas := v;⁻ nf_args (r_cat_l i ⋅ o ⦇ a ⦈)
        |}
  end rewrite c_view_cat_simpl_l.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
i: Δ ∋ cut_ty
((fun _ : T1 => nf_to_obs Δ) <$>
 Ret'
   (i
    ⋅ o
      ⦇ nf_args (r_cat_l i ⋅ o ⦇ a ⦈)
        ⊛ [a_id, bicollapse v red_pas] ⦈))
≊ Ret' (i ⋅ o)
      apply it_eq_unstep; cbn; do 2 econstructor.
    -
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
((fun _ : T1 => nf_to_obs Δ) <$>
 match c_view_cat (r_cat_r j) with
 | Vcat_l i =>
     Ret'
       (i
        ⋅ o
          ⦇ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
            ⊛ [a_id, bicollapse v red_pas] ⦈)
 | Vcat_r j0 =>
     eval
       (bicollapse v red_pas cut_ty j0 ⊙ o
        ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
          ⊛ [a_id, bicollapse v red_pas] ⦘)
 end)
≊ match c_view_cat (r_cat_r j) with
  | Vcat_l i => Ret' (i ⋅ o)
  | Vcat_r j0 =>
      reduce
        {|
          red_ctx := red_ctx ▶ₓ dom o;
          red_act := m_strat_resp red_pas (j0 ⋅ o);
          red_pas := v;⁻ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
        |}
  end rewrite c_view_cat_simpl_r.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
      ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ reduce
    {|
      red_ctx := red_ctx ▶ₓ dom o;
      red_act := m_strat_resp red_pas (j ⋅ o);
      red_pas := v;⁻ nf_args (r_cat_r j ⋅ o ⦇ a ⦈)
    |}
      unfold reduce; cbn; unfold nf_args, cut_r, fill_args; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
      assert (H : (bicollapse v red_pas cut_ty j ⊙ o ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘)
                  = ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o ⦗ r_cat_rr ᵣ⊛ a_id ⦘
       ₜ⊛ [a_id, [bicollapse v red_pas, a ⊛ [a_id, bicollapse v red_pas]]])).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])             
        rewrite app_sub, <- v_sub_sub.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j
 ᵥ⊛ r_emb r_cat3_1
    ⊛ [a_id,
      [bicollapse v red_pas,
      a ⊛ [a_id, bicollapse v red_pas]]]) ⊙ o
⦗ (r_cat_rr ᵣ⊛ a_id)
  ⊛ [a_id,
    [bicollapse v red_pas,
    a ⊛ [a_id, bicollapse v red_pas]]] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])

        (* AAAAA setoid rewriting!!!! *)
        etransitivity; cycle 1.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
?y =
(ₐ↓ red_pas cut_ty j
 ᵥ⊛ r_emb r_cat3_1
    ⊛ [a_id,
      [bicollapse v red_pas,
      a ⊛ [a_id, bicollapse v red_pas]]]) ⊙ o
⦗ (r_cat_rr ᵣ⊛ a_id)
  ⊛ [a_id,
    [bicollapse v red_pas,
    a ⊛ [a_id, bicollapse v red_pas]]] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ = 
?y
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
        unshelve erewrite v_sub_proper.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
val (Δ +▶ Game.join_pol Game.Pas red_ctx) cut_ty
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
(Δ +▶ Game.join_pol Game.Pas red_ctx) =[ val ]> Δ
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
?y =
(?y0 ᵥ⊛ ?y1) ⊙ o
⦗ (r_cat_rr ᵣ⊛ a_id)
  ⊛ [a_id,
    [bicollapse v red_pas,
    a ⊛ [a_id, bicollapse v red_pas]]] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
ₐ↓ red_pas cut_ty j = ?y0
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
r_emb r_cat3_1
⊛ [a_id,
  [bicollapse v red_pas,
  a ⊛ [a_id, bicollapse v red_pas]]] ≡ₐ 
?y1
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ = 
?y
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
        5: {
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
r_emb r_cat3_1
⊛ [a_id,
  [bicollapse v red_pas,
  a ⊛ [a_id, bicollapse v red_pas]]] ≡ₐ 
?y1 rewrite (a_ren_r_simpl _ r_cat3_1 _).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
r_cat3_1
ᵣ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]] ≡ₐ 
?y1
             now rewrite r_cat3_1_simpl; eauto.
           }
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
val (Δ +▶ Game.join_pol Game.Pas red_ctx) cut_ty
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
?y =
(?y0 ᵥ⊛ [a_id, bicollapse v red_pas]) ⊙ o
⦗ (r_cat_rr ᵣ⊛ a_id)
  ⊛ [a_id,
    [bicollapse v red_pas,
    a ⊛ [a_id, bicollapse v red_pas]]] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
ₐ↓ red_pas cut_ty j = ?y0
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ = 
?y
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
        3,4: reflexivity.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ [a_id, bicollapse v red_pas])
⊙ o
⦗ (r_cat_rr ᵣ⊛ a_id)
  ⊛ [a_id,
    [bicollapse v red_pas,
    a ⊛ [a_id, bicollapse v red_pas]]] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])

        change (?r ᵣ⊛ a_id)%asgn with (r_emb r); rewrite a_ren_r_simpl.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ [a_id, bicollapse v red_pas])
⊙ o
⦗ r_cat_rr
  ᵣ⊛ [a_id,
     [bicollapse v red_pas,
     a ⊛ [a_id, bicollapse v red_pas]]] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
subst_monoid_laws val
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
        unfold r_cat_rr; rewrite a_ren_l_comp.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ [a_id, bicollapse v red_pas])
⊙ o
⦗ r_cat_r
  ᵣ⊛ (r_cat_r
      ᵣ⊛ [a_id,
         [bicollapse v red_pas,
         a ⊛ [a_id, bicollapse v red_pas]]]) ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
subst_monoid_laws val
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
        rewrite 2 a_cat_proj_r.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ [a_id, bicollapse v red_pas])
⊙ o ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
subst_monoid_laws val
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])

        pose proof (H := collapse_fix_pas v red_pas _ j).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: (@eq
 ∘ (fun
      _ : Game.join_pol (Game.p_switch Game.Pas)
            red_ctx ∋ cut_ty => 
    val Δ cut_ty)) j
  ((ₐ↓ red_pas ⊛ [a_id, bicollapse v red_pas])%asgn
     cut_ty j) (bicollapse v red_pas cut_ty j)
bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ [a_id, bicollapse v red_pas])
⊙ o ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
subst_monoid_laws val
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
        cbn in H; now rewrite H.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
subst_monoid_laws val
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
        exact _.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])

      pose (xx := bicollapse v red_pas cut_ty j ⊙ o ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘).
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
H: bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘ =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
xx:= bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘: conf Δ
((fun _ : T1 => nf_to_obs Δ) <$>
 eval
   (bicollapse v red_pas cut_ty j ⊙ o
    ⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘))
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
      change (bicollapse v _ _ _ ⊙ o ⦗ _ ⦘) with xx in H |- *.
T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Δ: C
red_ctx: Game.ogs_ctx
u: conf (Δ +▶ Game.join_pol Game.Act red_ctx)
v: ogs_env Δ Game.Act red_ctx
red_pas: m_strat_pas Δ red_ctx
cut_ty: T
o: obs cut_ty
a: dom o =[ val
]> (Δ +▶
    Game.join_pol Game.Act
      (Strategy.red_ctx
         {|
           red_ctx := red_ctx;
           red_act :=
             {| ms_conf := u; ms_env := v |};
           red_pas := red_pas
         |}))
j: Game.join_pol Game.Act
  (Strategy.red_ctx
     {|
       red_ctx := red_ctx;
       red_act := {| ms_conf := u; ms_env := v |};
       red_pas := red_pas
     |}) ∋ cut_ty
xx:= bicollapse v red_pas cut_ty j ⊙ o
⦗ a ⊛ [a_id, bicollapse v red_pas] ⦘: conf Δ
H: xx =
(ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
⦗ r_cat_rr ᵣ⊛ a_id ⦘
ₜ⊛ [a_id,
   [bicollapse v red_pas,
   a ⊛ [a_id, bicollapse v red_pas]]]
((fun _ : T1 => nf_to_obs Δ) <$> eval xx)
≊ evalₒ
    ((ₐ↓ red_pas cut_ty j ᵥ⊛ r_emb r_cat3_1) ⊙ o
     ⦗ r_cat_rr ᵣ⊛ a_id ⦘
     ₜ⊛ [a_id,
        [bicollapse v red_pas,
        a ⊛ [a_id, bicollapse v red_pas]]])
      now rewrite H.
  Qed.