Congruence (Def 6.1)

We prove in this module that weak bisimilarity is a congruence for composition. The proof makes a slight technical side step: we prove the composition to be equivalent to an alternate definition, dully named compo_alt.

Indeed, congruence is a very easy result, demanding basically no assumption. What is actually hard, is to manage weak bisimilarity proofs, which in contrast to strong bisimilarity can be hard to tame: instead of synchronizing, at every step they can eat any number of Tau node on either side, forcing us to do complex inductions in the middle of our bisimilarity proofs.

Because of this, since our main definition compo is the specific case of composition of two instances of the machine strategy in the OGS game, we know much more than what we actually care about. Hence we define the much more general compo_alt composing any two abstract strategy for the OGS game and prove that one congruent w.r.t. weak bisimilarity. We then connect these two alternative definitions with a strong bisimilarity, much more structured, hence easy to prove.

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}.
  Context {ML : machine_laws val conf obs} {VV : var_assumptions val}.

We start off by defining this new, opaque composition.

  Record compo_alt_t (Δ : C) : Type := AltT {
    alt_ctx : ogs_ctx ;
    alt_act : ogs_act (obs:=obs) Δ alt_ctx ;
    alt_pas : ogs_pas (obs:=obs) Δ alt_ctx
  } .
  #[global] Arguments AltT {Δ Φ} u v : rename.
  #[global] Arguments alt_ctx {Δ}.
  #[global] Arguments alt_act {Δ}.
  #[global] Arguments alt_pas {Δ}.

  Definition compo_alt_body {Δ}
    : compo_alt_t Δ -> delay (compo_alt_t Δ + obs∙ Δ)
    := cofix _compo_body x :=
        go match x.(alt_act).(_observe) with
            | RetF r => RetD (inr r)
            | TauF t => TauD (_compo_body (AltT t x.(alt_pas)))
            | VisF e k => RetD (inl (AltT (x.(alt_pas) e) k))
            end .

  Definition compo_alt {Δ a} (u : ogs_act Δ a) (v : ogs_pas Δ a) : delay (obs∙ Δ)
    := iter_delay compo_alt_body (AltT u v).

Now we define our bisimulation candidates, for weak and strong bisimilarity.

  Variant alt_t_weq Δ : relation (compo_alt_t Δ) :=
  | AltWEq {Φ u1 u2 v1 v2}
    : u1 ≈ u2
      -> h_pasvR ogs_hg (it_wbisim (eqᵢ _)) _ v1 v2
      -> alt_t_weq Δ (AltT (Φ:=Φ) u1 v1) (AltT (Φ:=Φ) u2 v2).

  Variant alt_t_seq Δ : relation (compo_alt_t Δ) :=
  | AltSEq {Φ u1 u2 v1 v2}
    : u1 ≊ u2
      -> h_pasvR ogs_hg (it_eq (eqᵢ _)) _ v1 v2
      -> alt_t_seq Δ (AltT (Φ:=Φ) u1 v1) (AltT (Φ:=Φ) u2 v2).

And prove the tedious but direct weak congruence.

  #[global] Instance compo_alt_proper {Δ a}
    : Proper (it_wbisim (eqᵢ _) a
                ==> h_pasvR ogs_hg (it_wbisim (eqᵢ _)) a
                ==> it_wbisim (eqᵢ _) T1_0)
        (@compo_alt Δ a).
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: ogs_ctx
Proper
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)) a ==>
   h_pasvR ogs_hg
     (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) a ==>
   it_wbisim (eqᵢ (fun _ : T1 => obs ∙ Δ)) T1_0)
  compo_alt
    intros x y H1 u v H2.
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: ogs_ctx
x, y: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a
H1: x ≈ y
u, v: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) a
H2: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  a u v
compo_alt x u ≈ compo_alt y v
    unshelve eapply (iter_weq (RX := fun _ => alt_t_weq Δ)); [ | now 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
a: ogs_ctx
x, y: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) a
H1: x ≈ y
u, v: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) a
H2: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  a u v
dpointwise_relation
  (fun i : T1 =>
   (alt_t_weq Δ ==>
    it_wbisim
      (sumᵣ (fun _ : T1 => alt_t_weq Δ)
         (eqᵢ (fun _ : T1 => obs ∙ Δ))) i)%signature)
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (compo_alt_t Δ ->
       itree ∅ₑ
         ((fun _ : T1 => compo_alt_t Δ) +ᵢ
          (fun _ : T1 => obs ∙ Δ)) x) in
    compo_alt_body)
  (fun pat : T1 =>
   let
   'T1_0 as x := pat
    return
      (compo_alt_t Δ ->
       itree ∅ₑ
         ((fun _ : T1 => compo_alt_t Δ) +ᵢ
          (fun _ : T1 => obs ∙ Δ)) x) in
    compo_alt_body)
    clear a x y H1 u v H2; intros [] ?? [ ????? Hu Hv ].
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, y: compo_alt_t Δ
Φ: ogs_ctx
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hu: u1 ≈ u2
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
it_wbisim
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) T1_0
  (compo_alt_body
     {| alt_ctx := Φ; alt_act := u1; alt_pas := v1 |})
  (compo_alt_body
     {| alt_ctx := Φ; alt_act := u2; alt_pas := v2 |})
    revert u1 u2 Hu; unfold it_wbisim; coinduction R CIH; intros u1 u2 Hu.
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
Hu: gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2
it_wbisim_bt ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {| alt_ctx := Φ; alt_act := u1; alt_pas := v1 |})
  (compo_alt_body
     {| alt_ctx := Φ; alt_act := u2; alt_pas := v2 |})
    apply it_wbisim_step in Hu; cbn in *; unfold observe in Hu.
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
Hu: it_wbisimF ogs_e
  (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ (_observe u1) (_observe u2)
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
    destruct Hu as [ ? ? r1 r2 rr ].
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
x1, x2: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) x1
r2: it_eat Φ (_observe u2) x2
rr: it_eqF ogs_e (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ x1 x2
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
    dependent destruction rr.
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r0: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r0)
r3: obs ∙ Δ
r2: it_eat Φ (_observe u2) (RetF r3)
r_rel: eqᵢ (fun _ : ogs_ctx => obs ∙ Δ) Φ r0 r3
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r0: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r0)
r3: obs ∙ Δ
r2: it_eat Φ (_observe u2) (RetF r3)
r_rel: eqᵢ (fun _ : ogs_ctx => obs ∙ Δ) Φ r0 r3
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end dependent destruction r_rel; unshelve 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
it_eat T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end ?x1
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
it_eat T1_0
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end ?x2
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
it_eqF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0 
  ?x1 ?x2
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) T1_0 exact (RetF (inr r3)).
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) T1_0 exact (RetF (inr r3)).
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
it_eat T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end (RetF (inr r3)) remember (_observe u1) eqn:H; clear 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
i: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ i (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end (RetF (inr r3))
        remember (RetF (E:=ogs_e) r3) eqn: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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
i, i0: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
H: i0 = RetF r3
r1: it_eat Φ i i0
r2: it_eat Φ (_observe u2) i0
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end (RetF (inr r3))
        induction r1; [ now rewrite H | 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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
it_eat T1_0
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end (RetF (inr r3)) remember (_observe u2) eqn:H; clear 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
i: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ i (RetF r3)
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end (RetF (inr r3))
        remember (RetF (E:=ogs_e) r3) eqn: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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
i0: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
H: i0 = RetF r3
r1: it_eat Φ (_observe u1) i0
i: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ i i0
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end (RetF (inr r3))
        induction r2; [ now rewrite H | 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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r3: obs ∙ Δ
r1: it_eat Φ (_observe u1) (RetF r3)
r2: it_eat Φ (_observe u2) (RetF r3)
it_eqF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  (RetF (inr r3)) (RetF (inr r3)) now repeat 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end unshelve 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eat T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end ?x1
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eat T1_0
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end ?x2
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eqF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0 
  ?x1 ?x2
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) T1_0 exact (TauD (compo_alt_body (AltT t1 v1))).
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) T1_0 exact (TauD (compo_alt_body (AltT t2 v2))).
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eat T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t1; alt_pas := v1
          |}) remember (_observe u1) eqn:H; clear 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
i: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ i (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t1; alt_pas := v1
          |})
        remember (TauF t1) eqn: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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
i, i0: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
H: i0 = TauF t1
r1: it_eat Φ i i0
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t1; alt_pas := v1
          |})
        induction r1; [ now rewrite H | auto ].
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eat T1_0
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t2; alt_pas := v2
          |}) remember (_observe u2) eqn:H; clear 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
i: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ i (TauF t2)
t_rel: t1 ≈ t2
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t2; alt_pas := v2
          |})
        remember (TauF t2) eqn: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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
i, i0: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
H: i0 = TauF t2
r2: it_eat Φ i i0
t_rel: t1 ≈ t2
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t2; alt_pas := v2
          |})
        induction r2; [ now rewrite H | auto ].
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2, t1: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ (_observe u1) (TauF t1)
t2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ (_observe u2) (TauF t2)
t_rel: t1 ≈ t2
it_eqF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t1; alt_pas := v1
          |})
  (TauD compo_alt_body
          {|
            alt_ctx := Φ; alt_act := t2; alt_pas := v2
          |}) auto.
    -
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_wbisimF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end unshelve 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end ?x1
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end ?x2
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eqF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0 
  ?x1 ?x2
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) T1_0 exact (RetF (inl (AltT (v1 q) k1))).
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
itree' ∅ₑ
  ((fun _ : T1 => compo_alt_t Δ) +ᵢ
   (fun _ : T1 => obs ∙ Δ)) T1_0 exact (RetF (inl (AltT (v2 q) k2))).
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match _observe u1 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v1 q;
          alt_pas := k1
        |})) remember (_observe u1) eqn:H; clear 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
i: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r1: it_eat Φ i (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v1 q;
          alt_pas := k1
        |}))
        remember (VisF q k1) eqn: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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
i, i0: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
H: i0 = VisF q k1
r1: it_eat Φ i i0
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v1
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v1 e;
             alt_pas := k
           |})
  end
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v1 q;
          alt_pas := k1
        |}))
        induction r1; [ now rewrite H | auto ].
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match _observe u2 with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v2 q;
          alt_pas := k2
        |})) remember (_observe u2) eqn:H; clear 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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
i: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
r2: it_eat Φ i (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v2 q;
          alt_pas := k2
        |}))
        remember (VisF q k2) eqn: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
x, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
i, i0: itree' ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
H: i0 = VisF q k2
r2: it_eat Φ i i0
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eat T1_0
  match i with
  | RetF r => RetF (inr r)
  | TauF t =>
      TauF
        (compo_alt_body
           {|
             alt_ctx := Φ; alt_act := t; alt_pas := v2
           |})
  | VisF e k =>
      RetF
        (inl
           {|
             alt_ctx := Φ ▶ₓ m_dom e;
             alt_act := v2 e;
             alt_pas := k
           |})
  end
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v2 q;
          alt_pas := k2
        |}))
        induction r2; [ now rewrite H | auto ].
      *
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, y: compo_alt_t Δ
Φ: ogs_ctx
v1, v2: h_pasv ogs_hg
  (itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)) Φ
Hv: h_pasvR ogs_hg
  (it_wbisim (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ)))
  Φ v1 v2
R: relᵢ
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
  (itree ∅ₑ
     ((fun _ : T1 => compo_alt_t Δ) +ᵢ
      (fun _ : T1 => obs ∙ Δ)))
CIH: forall
  u1
   u2 : itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
          Φ,
gfp
  (it_wbisim_map ogs_e
     (eqᵢ (fun _ : ogs_ctx => obs ∙ Δ))) Φ u1 u2 ->
it_wbisim_t ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ))) R T1_0
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u1;
       alt_pas := v1
     |})
  (compo_alt_body
     {|
       alt_ctx := Φ;
       alt_act := u2;
       alt_pas := v2
     |})
u1, u2: itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ) Φ
q: e_qry Φ
k1: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r1: it_eat Φ (_observe u1) (VisF q k1)
k2: forall x : e_rsp q,
itree ogs_e (fun _ : ogs_ctx => obs ∙ Δ)
  (e_nxt x)
r2: it_eat Φ (_observe u2) (VisF q k2)
k_rel: forall r : e_rsp q, k1 r ≈ k2 r
it_eqF ∅ₑ
  (sumᵣ (fun _ : T1 => alt_t_weq Δ)
     (eqᵢ (fun _ : T1 => obs ∙ Δ)))
  (it_wbisim_t ∅ₑ
     (sumᵣ (fun _ : T1 => alt_t_weq Δ)
        (eqᵢ (fun _ : T1 => obs ∙ Δ))) R) T1_0
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v1 q;
          alt_pas := k1
        |}))
  (RetF
     (inl
        {|
          alt_ctx := g_next q;
          alt_act := v2 q;
          alt_pas := k2
        |})) unshelve (do 3 econstructor); eauto.
   Qed.