Built with Alectryon, running Coq+SerAPI v8.17.0+0.17.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.

Interaction Trees: Theory of the structure

We collect in these file the main lemmas capturing the applicative, monadic, and iterative structure of itrees.

Section withE.
  Context {I} {E : event I I}.

fmap respects strong bisimilarity.

  
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)

Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) fmap
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)

Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) fmap
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g

dpointwise_relation (fun i : I => (it_eq RX (i:=i) ==> it_eq RY (i:=i))%signature) (fmap f) (fmap g)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g

forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> gfp (it_eq_map E RY) a (f <$> x) (g <$> y)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: gfp (it_eq_map E RX) i x y

it_eq_bt E RY R i (f <$> x) (g <$> y)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: it_eq_map E RX (gfp (it_eq_map E RX)) i x y

it_eq_bt E RY R i (f <$> x) (g <$> y)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f <$> x) (g <$> y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2

it_eqF E RY (it_eq_t E RY R) i (RetF (f i r1)) (RetF (g i r2))
econstructor; now apply H1. Qed.

fmap respects weak bisimilarity.

  
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)

Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_wbisim RX i ==> it_wbisim RY i)) fmap
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)

Proper (dpointwise_relation (fun i : I => RX i ==> RY i) ==> dpointwise_relation (fun i : I => it_wbisim RX i ==> it_wbisim RY i)) fmap
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g

dpointwise_relation (fun i : I => (it_wbisim RX i ==> it_wbisim RY i)%signature) (fmap f) (fmap g)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g

forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> gfp (it_wbisim_map E RY) a (f <$> x) (g <$> y)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: gfp (it_wbisim_map E RX) i x y

it_wbisim_bt E RY R i (f <$> x) (g <$> y)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: dpointwise_relation (fun i : I => (RX i ==> RY i)%signature) f g
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: it_wbisim_map E RX (gfp (it_wbisim_map E RX)) i x y

it_wbisim_bt E RY R i (f <$> x) (g <$> y)
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
h: it_wbisimF E RX (gfp (it_wbisim_map E RX)) i (_observe x) (_observe y)

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
x1, x2: itree' E X i
r1: it_eat i (_observe x) x1
r2: it_eat i (_observe y) x2
rr: it_eqF E RX (gfp (it_wbisim_map E RX)) i x1 x2

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2
it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)
it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

itree' E Y i
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3
itree' E Y i
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3
it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end ?x1
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3
it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end ?x2
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3
it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

itree' E Y i
exact (RetF (f i r0)).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

itree' E Y i
exact (RetF (g i r3)).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (RetF (f i r0))
I: Type
E: event I I
X, Y: psh I
f: forall a : I, X a -> Y a
i: I
r0: X i
ot: itree' E X i
r1: it_eat i ot (RetF r0)

it_eat i match ot with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (RetF (f i r0))
I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
r0: X i
r1: it_eat i (observe t1) (RetF r0)
IHr1: forall (Y : psh I) (f : forall a : I, X a -> Y a) (r1 : X i), RetF r0 = RetF r1 -> it_eat i match observe t1 with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (RetF (f i r1))
Y: psh I
f: forall a : I, X a -> Y a

it_eat i (observe (f <$> t1)) (RetF (f i r0))
exact (IHr1 Y f r0 eq_refl).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (RetF (g i r3))
I: Type
E: event I I
X, Y: psh I
g: forall a : I, X a -> Y a
i: I
r3: X i
ot: itree' E X i
r2: it_eat i ot (RetF r3)

it_eat i match ot with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (RetF (g i r3))
I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
r3: X i
r2: it_eat i (observe t1) (RetF r3)
IHr2: forall (Y : psh I) (g : forall a : I, X a -> Y a) (r4 : X i), RetF r3 = RetF r4 -> it_eat i match observe t1 with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (RetF (g i r4))
Y: psh I
g: forall a : I, X a -> Y a

it_eat i (observe (g <$> t1)) (RetF (g i r3))
exact (IHr2 Y g r3 eq_refl).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

it_eqF E RY (it_wbisim_t E RY R) i (RetF (f i r0)) (RetF (g i r3))
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
r0: X i
r1: it_eat i (_observe x) (RetF r0)
r3: X i
r2: it_eat i (_observe y) (RetF r3)
r_rel: RX i r0 r3

RY i (f i r0) (g i r3)
now apply H1.
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

itree' E Y i
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2
itree' E Y i
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2
it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end ?x1
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2
it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end ?x2
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2
it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

itree' E Y i
exact (TauF (f <$> t1)).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

itree' E Y i
exact (TauF (g <$> t2)).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (TauF (f <$> t1))
I: Type
E: event I I
X, Y: psh I
f: forall a : I, X a -> Y a
i: I
t1: itree E X i
ot: itree' E X i
r1: it_eat i ot (TauF t1)

it_eat i match ot with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (TauF (f <$> t1))
I: Type
E: event I I
X: psh I
i: I
t0, t1: itree E X i
r1: it_eat i (observe t0) (TauF t1)
IHr1: forall (Y : psh I) (f : forall a : I, X a -> Y a) (t2 : itree E X i), TauF t1 = TauF t2 -> it_eat i match observe t0 with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (TauF (f <$> t2))
Y: psh I
f: forall a : I, X a -> Y a

it_eat i (observe (f <$> t0)) (TauF (f <$> t1))
exact (IHr1 Y f t1 eq_refl).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (TauF (g <$> t2))
I: Type
E: event I I
X, Y: psh I
g: forall a : I, X a -> Y a
i: I
t2: itree E X i
ot: itree' E X i
r2: it_eat i ot (TauF t2)

it_eat i match ot with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (TauF (g <$> t2))
I: Type
E: event I I
X: psh I
i: I
t1, t2: itree E X i
r2: it_eat i (observe t1) (TauF t2)
IHr2: forall (Y : psh I) (g : forall a : I, X a -> Y a) (t3 : itree E X i), TauF t2 = TauF t3 -> it_eat i match observe t1 with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (TauF (g <$> t3))
Y: psh I
g: forall a : I, X a -> Y a

it_eat i (observe (g <$> t1)) (TauF (g <$> t2))
exact (IHr2 Y g t2 eq_refl).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

it_eqF E RY (it_wbisim_t E RY R) i (TauF (f <$> t1)) (TauF (g <$> t2))
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y, t1: itree E X i
r1: it_eat i (_observe x) (TauF t1)
t2: itree E X i
r2: it_eat i (_observe y) (TauF t2)
t_rel: gfp (it_wbisim_map E RX) i t1 t2

it_wbisim_t E RY R i (f <$> t1) (g <$> t2)
now apply CIH.
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

itree' E Y i
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)
itree' E Y i
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)
it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end ?x1
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)
it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end ?x2
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)
it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

itree' E Y i
exact (VisF q (fun r => f <$> k1 r)).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

itree' E Y i
exact (VisF q (fun r => g <$> k2 r)).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

it_eat i match _observe x with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (VisF q (fun r : e_rsp q => f <$> k1 r))
I: Type
E: event I I
X, Y: psh I
f: forall a : I, X a -> Y a
i: I
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
ot: itree' E X i
r1: it_eat i ot (VisF q k1)

it_eat i match ot with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (VisF q (fun r : e_rsp q => f <$> k1 r))
I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (observe t1) (VisF q k1)
IHr1: forall (Y : psh I) (f : forall a : I, X a -> Y a) (q0 : e_qry i) (k2 : forall x : e_rsp q0, itree E X (e_nxt x)), VisF q k1 = VisF q0 k2 -> it_eat i match observe t1 with | RetF r => RetF (f i r) | TauF t => TauF (f <$> t) | VisF e k => VisF e (fun r : e_rsp e => f <$> k r) end (VisF q0 (fun r : e_rsp q0 => f <$> k2 r))
Y: psh I
f: forall a : I, X a -> Y a

it_eat i (observe (f <$> t1)) (VisF q (fun r : e_rsp q => f <$> k1 r))
exact (IHr1 Y f q k1 eq_refl).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

it_eat i match _observe y with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (VisF q (fun r : e_rsp q => g <$> k2 r))
I: Type
E: event I I
X, Y: psh I
g: forall a : I, X a -> Y a
i: I
q: e_qry i
k2: forall x : e_rsp q, itree E X (e_nxt x)
ot: itree' E X i
r2: it_eat i ot (VisF q k2)

it_eat i match ot with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (VisF q (fun r : e_rsp q => g <$> k2 r))
I: Type
E: event I I
X: psh I
i: I
t1: itree E X i
q: e_qry i
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (observe t1) (VisF q k2)
IHr2: forall (Y : psh I) (g : forall a : I, X a -> Y a) (q0 : e_qry i) (k3 : forall x : e_rsp q0, itree E X (e_nxt x)), VisF q k2 = VisF q0 k3 -> it_eat i match observe t1 with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end (VisF q0 (fun r : e_rsp q0 => g <$> k3 r))
Y: psh I
g: forall a : I, X a -> Y a

it_eat i (observe (g <$> t1)) (VisF q (fun r : e_rsp q => g <$> k2 r))
exact (IHr2 Y g q k2 eq_refl).
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

it_eqF E RY (it_wbisim_t E RY R) i (VisF q (fun r : e_rsp q => f <$> k1 r)) (VisF q (fun r : e_rsp q => g <$> k2 r))
I: Type
E: event I I
X: psh I
RX: forall x : I, relation (X x)
Y: psh I
RY: forall x : I, relation (Y x)
f, g: forall a : I, X a -> Y a
H1: forall a : I, (RX a ==> RY a)%signature (f a) (g a)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_wbisim_map E RX) a x y -> it_wbisim_t E RY R a (f <$> x) (g <$> y)
i: I
x, y: itree E X i
q: e_qry i
k1: forall x : e_rsp q, itree E X (e_nxt x)
r1: it_eat i (_observe x) (VisF q k1)
k2: forall x : e_rsp q, itree E X (e_nxt x)
r2: it_eat i (_observe y) (VisF q k2)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k1 r) (k2 r)

forall r : e_rsp q, it_wbisim_t E RY R (e_nxt r) (f <$> k1 r) (g <$> k2 r)
intro r; now apply CIH. Qed.

subst respects weak bisimilarity.

  
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y

Proper (dpointwise_relation (fun i : I => RX i ==> it_eq RY (i:=i)) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) subst
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y

Proper (dpointwise_relation (fun i : I => RX i ==> it_eq RY (i:=i)) ==> dpointwise_relation (fun i : I => it_eq RX (i:=i) ==> it_eq RY (i:=i))) subst
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y

forall x y : forall a : I, X a -> itree E Y a, (forall (a : I) (x0 y0 : X a), RX a x0 y0 -> gfp (it_eq_map E RY) a (x a x0) (y a y0)) -> forall (a : I) (x0 y0 : itree E X a), gfp (it_eq_map E RX) a x0 y0 -> gfp (it_eq_map E RY) a (x =<< x0) (y =<< y0)
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x, y: itree E X i
h2: gfp (it_eq_map E RX) i x y

it_eq_bt E RY R i (f =<< x) (g =<< y)
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x, y: itree E X i
h2: it_eq_map E RX (gfp (it_eq_map E RX)) i x y

it_eq_bt E RY R i (f =<< x) (g =<< y)
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2

it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
h3:= h1 i r1 r2 r_rel: gfp (it_eq_map E RY) i (f i r1) (g i r2)

it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
h3: it_eq_map E RY (gfp (it_eq_map E RY)) i (f i r1) (g i r2)

it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
h3: it_eqF E RY (gfp (it_eq_map E RY)) i (_observe (f i r1)) (_observe (g i r2))

it_eqF E RY (it_eq_t E RY R) i (_observe (f i r1)) (_observe (g i r2))
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
t1, t2: itree E Y i
t_rel: gfp (it_eq_map E RY) i t1 t2

it_eq_t E RY R i t1 t2
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
q: e_qry i
k1, k2: forall x : e_rsp q, itree E Y (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RY) (e_nxt r) (k1 r) (k2 r)
forall r : e_rsp q, it_eq_t E RY R (e_nxt r) (k1 r) (k2 r)
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
t1, t2: itree E Y i
t_rel: gfp (it_eq_map E RY) i t1 t2

it_eq_t E RY R i t1 t2
I: Type
E: event I I
X, Y: psh I
RX: relᵢ X X
RY: relᵢ Y Y
f, g: forall a : I, X a -> itree E Y a
h1: forall (a : I) (x y : X a), RX a x y -> gfp (it_eq_map E RY) a (f a x) (g a y)
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (a : I) (x y : itree E X a), gfp (it_eq_map E RX) a x y -> it_eq_t E RY R a (f =<< x) (g =<< y)
i: I
x0: itree E X i
r1, r2: X i
r_rel: RX i r1 r2
q: e_qry i
k1, k2: forall x : e_rsp q, itree E Y (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RY) (e_nxt r) (k1 r) (k2 r)
r: e_rsp q
it_eq_t E RY R (e_nxt r) (k1 r) (k2 r)
all: now apply (gfp_t (it_eq_map E RY)). Qed.

A slight generalization of the monad law t ≊ t >>= η.

  
I: Type
E: event I I
X, Y: psh I
RX: relᵢ Y Y
H: Reflexiveᵢ RX
f: X ⇒ᵢ Y
i: I
t: itree E X i

it_eq RX (f <$> t) (t >>= (fun (i : I) (x : X i) => Ret' (f i x)))
I: Type
E: event I I
X, Y: psh I
RX: relᵢ Y Y
H: Reflexiveᵢ RX
f: X ⇒ᵢ Y
i: I
t: itree E X i

it_eq RX (f <$> t) (t >>= (fun (i : I) (x : X i) => Ret' (f i x)))
I: Type
E: event I I
X, Y: psh I
RX: relᵢ Y Y
H: Reflexiveᵢ RX
f: X ⇒ᵢ Y
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E X i), it_eq_t E RX R i (f <$> t0) (t0 >>= (fun (i0 : I) (x : X i0) => Ret' (f i0 x)))
i: I
t: itree E X i

it_eq_bt E RX R i (f <$> t) (t >>= (fun (i : I) (x : X i) => Ret' (f i x)))
cbn; destruct (_observe t); auto. Qed.
I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I

Proper (it_eat' i ==> it_eat' i) (subst f i)
I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I

Proper (it_eat' i ==> it_eat' i) (subst f i)
I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I
x, y: itree E X i
H: it_eat i (_observe x) (_observe y)

it_eat i match _observe x with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end match _observe y with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end
I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I
x, y: itree E X i
_x: itree' E X i
H: it_eat i _x (_observe y)

it_eat i match _x with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end match _observe y with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end
I: Type
E: event I I
X, Y: psh I
f: X ⇒ᵢ itree E Y
i: I
x, y: itree E X i
_x, _y: itree' E X i
H: it_eat i _x _y

it_eat i match _x with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end match _y with | RetF r => _observe (f i r) | TauF t => TauF (f =<< t) | VisF e k => VisF e (fun r : e_rsp e => f =<< k r) end
dependent induction H; now econstructor. Qed.

Composition law of bind.

  
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X i

it_eq RZ ((x >>= f) >>= g) (x >>= (f >=> g))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X i

it_eq RZ ((x >>= f) >>= g) (x >>= (f >=> g))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))
i: I
x: itree E X i

it_eq_bt E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))
i: I
x: itree E X i
r: X i

it_eqF E RZ (it_eq_t E RZ R) i match _observe (f i r) with | RetF r => _observe (g i r) | TauF t => TauF (g =<< t) | VisF e k => VisF e (fun r : e_rsp e => g =<< k r) end match _observe (f i r) with | RetF r => _observe (g i r) | TauF t => TauF (g =<< t) | VisF e k => VisF e (fun r : e_rsp e => g =<< k r) end
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((x >>= f) >>= g) (x >>= (f >=> g))
i: I
x: itree E X i
r: X i
r0: Y i

it_eqF E RZ (it_eq_t E RZ R) i (_observe (g i r0)) (_observe (g i r0))
destruct ((g i r0).(_observe)); eauto. Qed.

Composition law of fmap.

  
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ Z
i: I
x: itree E X i

it_eq RZ (g <$> (f <$> x)) ((fun i : I => g i ∘ f i) <$> x)
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ Z
i: I
x: itree E X i

it_eq RZ (g <$> (f <$> x)) ((fun i : I => g i ∘ f i) <$> x)
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i (g <$> (f <$> x)) ((fun i0 : I => g i0 ∘ f i0) <$> x)
i: I
x: itree E X i

it_eq_bt E RZ R i (g <$> (f <$> x)) ((fun i : I => g i ∘ f i) <$> x)
cbn; destruct (x.(_observe)); eauto. Qed.

bind and fmap interaction.

  
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X i

it_eq RZ ((f <$> x) >>= g) (x >>= (fun i : I => g i ∘ f i))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
i: I
x: itree E X i

it_eq RZ ((f <$> x) >>= g) (x >>= (fun i : I => g i ∘ f i))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((f <$> x) >>= g) (x >>= (fun i0 : I => g i0 ∘ f i0))
i: I
x: itree E X i

it_eq_bt E RZ R i ((f <$> x) >>= g) (x >>= (fun i : I => g i ∘ f i))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ Y
g: Y ⇒ᵢ itree E Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i ((f <$> x) >>= g) (x >>= (fun i0 : I => g i0 ∘ f i0))
i: I
x: itree E X i
r: X i

it_eqF E RZ (it_eq_t E RZ R) i (_observe (g i (f i r))) (_observe (g i (f i r)))
destruct ((g i (f i r)).(_observe)); eauto. Qed.
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
i: I
x: itree E X i

it_eq RZ (g <$> (x >>= f)) (x >>= (fun i : I => fmap g i ∘ f i))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
i: I
x: itree E X i

it_eq RZ (g <$> (x >>= f)) (x >>= (fun i : I => fmap g i ∘ f i))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i (g <$> (x >>= f)) (x >>= (fun i0 : I => fmap g i0 ∘ f i0))
i: I
x: itree E X i

it_eq_bt E RZ R i (g <$> (x >>= f)) (x >>= (fun i : I => fmap g i ∘ f i))
I: Type
E: event I I
X, Y, Z: psh I
RZ: forall x : I, relation (Z x)
Reflexiveᵢ0: Reflexiveᵢ RZ
f: X ⇒ᵢ itree E Y
g: Y ⇒ᵢ Z
R: relᵢ (itree E Z) (itree E Z)
CIH: forall (i : I) (x : itree E X i), it_eq_t E RZ R i (g <$> (x >>= f)) (x >>= (fun i0 : I => fmap g i0 ∘ f i0))
i: I
x: itree E X i
r: X i

it_eqF E RZ (it_eq_t E RZ R) i match _observe (f i r) with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end match _observe (f i r) with | RetF r => RetF (g i r) | TauF t => TauF (g <$> t) | VisF e k => VisF e (fun r : e_rsp e => g <$> k r) end
destruct ((f i r).(_observe)); eauto. Qed.

Rewording composition law of bind.

  
I: Type
E: event I I
X, Y, Z: psh I
f: Y ⇒ᵢ itree E Z
g: X ⇒ᵢ itree E Y
i: I
x: itree E X i

((x >>= g) >>= f) ≊ (x >>= (g >=> f))
I: Type
E: event I I
X, Y, Z: psh I
f: Y ⇒ᵢ itree E Z
g: X ⇒ᵢ itree E Y
i: I
x: itree E X i

((x >>= g) >>= f) ≊ (x >>= (g >=> f))
apply bind_bind_com. Qed.

Proof of the up-to bind principle: we may close bisimulation candidates by prefixing related elements by bisimilar computations.

  Variant bindR {X1 X2 Y1 Y2} (RX : relᵢ X1 X2)
    (R : relᵢ (itree E X1) (itree E X2))
    (S : relᵢ (itree E Y1) (itree E Y2)) :
    relᵢ (itree E Y1) (itree E Y2) :=
    | BindR {i t1 t2 k1 k2}
        (u : R i t1 t2)
        (v : forall i x1 x2, RX i x1 x2 -> S i (k1 i x1) (k2 i x2))
      : bindR RX R S i (t1 >>= k1) (t2 >>= k2).
  Arguments BindR {X1 X2 Y1 Y2 RX R S i t1 t2 k1 k2}.
  Hint Constructors bindR : core.

Up-to bind is valid for strong bisimilarity.

  Program Definition bindR_eq_map {X1 X2 Y1 Y2} (RX : relᵢ X1 X2) : mon (relᵢ (itree E Y1) (itree E Y2)) :=
    {| body S := bindR RX (@it_eq _ E _ _ RX) S ;
       Hbody _ _ H _ _ _ '(BindR u v) := BindR u (fun i _ _ r => H _ _ _ (v i _ _ r)) |}.

  
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2

bindR_eq_map RX <= it_eq_t E RY
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2

bindR_eq_map RX <= it_eq_t E RY
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_eq RX t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eq_map E RY R i (k1 i x1) (k2 i x2)

bT (it_eq_map E RY) (bindR_eq_map RX) R i0 (t1 >>= k1) (t2 >>= k2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_eq_map E RX (gfp (it_eq_map E RX)) i0 t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eq_map E RY R i (k1 i x1) (k2 i x2)

bT (it_eq_map E RY) (bindR_eq_map RX) R i0 (t1 >>= k1) (t2 >>= k2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_eqF E RX (gfp (it_eq_map E RX)) i0 (_observe t1) (_observe t2)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r1: X1 i0
r2: X2 i0
r_rel: RX i0 r1 r2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (_observe (k1 i0 r1)) (_observe (k2 i0 r2))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
t3: itree E X2 i0
t_rel: gfp (it_eq_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (TauF (k1 =<< t0)) (TauF (k2 =<< t3))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (VisF q (fun r : e_rsp q => k1 =<< k0 r)) (VisF q (fun r : e_rsp q => k2 =<< k3 r))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r1: X1 i0
r2: X2 i0
r_rel: RX i0 r1 r2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (_observe (k1 i0 r1)) (_observe (k2 i0 r2))
refine (it_eqF_mon _ _ (id_T _ _ R) _ _ _ (v i0 _ _ r_rel)).
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
t3: itree E X2 i0
t_rel: gfp (it_eq_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (TauF (k1 =<< t0)) (TauF (k2 =<< t3))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
t3: itree E X2 i0
t_rel: gfp (it_eq_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

(bindR_eq_map RX ° it_eq_T E RY (bindR_eq_map RX)) R i0 (k1 =<< t0) (k2 =<< t3)
refine (BindR t_rel (fun i _ _ r => b_T (it_eq_map E RY) _ _ _ _ _ (v i _ _ r))).
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eqF E RY (it_eq_T E RY (bindR_eq_map RX) R) i0 (VisF q (fun r : e_rsp q => k1 =<< k0 r)) (VisF q (fun r : e_rsp q => k2 =<< k3 r))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x0: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
k_rel: forall r : e_rsp q, gfp (it_eq_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_eqF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
r: e_rsp q

(bindR_eq_map RX ° it_eq_T E RY (bindR_eq_map RX)) R (e_nxt r) (k1 =<< k0 r) (k2 =<< k3 r)
refine (BindR (k_rel r) (fun i _ _ r => b_T (it_eq_map E RY) _ _ _ _ _ (v i _ _ r))). Qed.

Up-to bind is valid for weak bisimilarity.

  Program Definition bindR_w_map {X1 X2 Y1 Y2} (RX : relᵢ X1 X2) : mon (relᵢ (itree E Y1) (itree E Y2)) :=
    {| body S := bindR RX (@it_wbisim _ E _ _ RX) S ;
       Hbody _ _ H _ _ _ '(BindR u v) := BindR u (fun i _ _ r => H _ _ _ (v i _ _ r)) |}.

  
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2

bindR_w_map RX <= it_wbisim_t E RY
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2

bindR_w_map RX <= it_wbisim_t E RY
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_wbisim RX i0 t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisim_map E RY R i (k1 i x1) (k2 i x2)

bT (it_wbisim_map E RY) (bindR_w_map RX) R i0 (t1 >>= k1) (t2 >>= k2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_wbisim_map E RX (gfp (it_wbisim_map E RX)) i0 t1 t2
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisim_map E RY R i (k1 i x1) (k2 i x2)

bT (it_wbisim_map E RY) (bindR_w_map RX) R i0 (t1 >>= k1) (t2 >>= k2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
u: it_wbisimF E RX (gfp (it_wbisim_map E RX)) i0 (_observe t1) (_observe t2)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2

it_eat i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end ?x1
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2
it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2
it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 ?x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2

it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2
it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
r0: X1 i0
r1: it_eat i0 (_observe t1) (RetF r0)
r3: X2 i0
r2: it_eat i0 (_observe t2) (RetF r3)
r_rel: RX i0 r0 r3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
x1: itree' E Y1 i0
x2: itree' E Y2 i0
s1: it_eat i0 (observe (k1 i0 r0)) x1
s2: it_eat i0 (observe (k2 i0 r3)) x2
ss: it_eqF E RY R i0 x1 x2

it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 x1 x2
now apply (it_eqF_mon _ _ (id_T _ _ R)).
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eat i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end ?x1
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 ?x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Tau' t0)) ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Tau' t0)) (_observe (k2 =<< Tau' t3))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_wbisim_T E RY (bindR_w_map RX) R i0 (k1 =<< t0) (k2 =<< t3)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
t0: itree E X1 i0
r1: it_eat i0 (_observe t1) (TauF t0)
t3: itree E X2 i0
r2: it_eat i0 (_observe t2) (TauF t3)
t_rel: gfp (it_wbisim_map E RX) i0 t0 t3
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

(bindR_w_map RX ° it_wbisim_T E RY (bindR_w_map RX)) R i0 (k1 =<< t0) (k2 =<< t3)
econstructor; [ apply t_rel | intros; now apply (b_T (it_wbisim_map E RY)), v ].
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_wbisimF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eat i0 match _observe t1 with | RetF r => _observe (k1 i0 r) | TauF t => TauF (k1 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k1 =<< k r) end ?x1
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 ?x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eat i0 match _observe t2 with | RetF r => _observe (k2 i0 r) | TauF t => TauF (k2 =<< t) | VisF e k => VisF e (fun r : e_rsp e => k2 =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Vis' q k0)) ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))

it_eqF E RY (it_wbisim_T E RY (bindR_w_map RX) R) i0 (_observe (k1 =<< Vis' q k0)) (_observe (k2 =<< Vis' q k3))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
r: e_rsp q

it_wbisim_T E RY (bindR_w_map RX) R (e_nxt r) (k1 =<< k0 r) (k2 =<< k3 r)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
R: relᵢ (itree E Y1) (itree E Y2)
i: I
x: itree E Y1 i
y: itree E Y2 i
i0: I
t1: itree E X1 i0
t2: itree E X2 i0
k1: forall x : I, X1 x -> itree E Y1 x
k2: forall x : I, X2 x -> itree E Y2 x
q: e_qry i0
k0: forall x : e_rsp q, itree E X1 (e_nxt x)
r1: it_eat i0 (_observe t1) (VisF q k0)
k3: forall x : e_rsp q, itree E X2 (e_nxt x)
r2: it_eat i0 (_observe t2) (VisF q k3)
k_rel: forall r : e_rsp q, gfp (it_wbisim_map E RX) (e_nxt r) (k0 r) (k3 r)
v: forall (i : I) (x1 : X1 i) (x2 : X2 i), RX i x1 x2 -> it_wbisimF E RY R i (observe (k1 i x1)) (observe (k2 i x2))
r: e_rsp q

(bindR_w_map RX ° it_wbisim_T E RY (bindR_w_map RX)) R (e_nxt r) (k1 =<< k0 r) (k2 =<< k3 r)
econstructor; [ apply k_rel | intros; now apply (b_T (it_wbisim_map E RY)), v ]. Qed.

Bisimilar equations have bisimilar iteration (weakly and strongly).

  
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)

forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq RY (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)

forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq RY (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b

it_eq_bt E RY R i (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
h1:= H i a b r: it_eq (sumᵣ RX RY) (f i a) (g i b)

it_eq_bt E RY R i (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
h1: it_eqF E (sumᵣ RX RY) (it_eq (sumᵣ RX RY)) i (_observe (f i a)) (_observe (g i b))

it_eqF E RY (it_eq_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r1: (X1 +ᵢ Y1) i
r2: (X2 +ᵢ Y2) i
r_rel: sumᵣ RX RY i r1 r2

it_eqF E RY (it_eq_t E RY R) i match r1 with | inl x => TauF (iter f i x) | inr y => RetF y end match r2 with | inl x => TauF (iter g i x) | inr y => RetF y end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2
it_eqF E RY (it_eq_t E RY R) i (TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1)) (TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)
it_eqF E RY (it_eq_t E RY R) i (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r)) (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r1: (X1 +ᵢ Y1) i
r2: (X2 +ᵢ Y2) i
r_rel: sumᵣ RX RY i r1 r2

it_eqF E RY (it_eq_t E RY R) i match r1 with | inl x => TauF (iter f i x) | inr y => RetF y end match r2 with | inl x => TauF (iter g i x) | inr y => RetF y end
destruct r_rel; eauto.
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2

it_eqF E RY (it_eq_t E RY R) i (TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1)) (TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2

it_eq_t E RY R i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2

it_eq_t E RY (it_eq_t E RY R) i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
t2: itree E (X2 +ᵢ Y2) i
t_rel: it_eq (sumᵣ RX RY) t1 t2

forall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_eq_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}
intros ? ? ? []; apply (tt_t (it_eq_map E RY)), (b_t (it_eq_map E RY)); cbn; eauto.
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)

it_eqF E RY (it_eq_t E RY R) i (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r)) (VisF q (fun r : e_rsp q => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)
r0: e_rsp q

it_eq_t E RY R (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)
r0: e_rsp q

it_eq_t E RY (it_eq_t E RY R) (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq (sumᵣ RX RY) (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_eq_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
k_rel: forall r : e_rsp q, it_eq (sumᵣ RX RY) (k1 r) (k2 r)
r0: e_rsp q

forall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_eq_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}
intros ? ? ? []; apply (bt_t (it_eq_map E RY)); cbn; eauto. Qed. #[global] Instance iter_proper_strong {X Y} {RX : relᵢ X X} {RY : relᵢ Y Y} : Proper (dpointwise_relation (fun i => RX i ==> it_eq (sumᵣ RX RY) (i:=i)) ==> dpointwise_relation (fun i => RX i ==> it_eq RY (i:=i))) (@iter I E X Y) := iter_cong_strong.
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)

forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim RY i (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)

forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim RY i (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b

it_wbisim_bt E RY R i (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
H1:= H i a b r: it_wbisim (sumᵣ RX RY) i (f i a) (g i b)

it_wbisim_bt E RY R i (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
H1: it_wbisim_map E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i (f i a) (g i b)

it_wbisim_bt E RY R i (iter f i a) (iter g i b)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
H1: it_wbisimF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i (_observe (f i a)) (_observe (g i b))

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r0: (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (RetF r0)
r3: (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (RetF r3)
r_rel: sumᵣ RX RY i r0 r3

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2
it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
r0: (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (RetF r0)
r3: (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (RetF r3)
r_rel: sumᵣ RX RY i r0 r3

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2
it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
H2:= H i x1 x2 H0: it_wbisim (sumᵣ RX RY) i (f i x1) (g i x2)

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
H2: it_wbisim_map E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i (f i x1) (g i x2)

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3

it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3
it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3
it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3

it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3
it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inl x1))) ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3

it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inl x1))) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Ret' (inl x2)))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
x1: X1 i
r1: it_eat i (_observe (f i a)) (RetF (inl x1))
x2: X2 i
r2: it_eat i (_observe (g i b)) (RetF (inl x2))
H0: RX i x1 x2
x0: itree' E (X1 +ᵢ Y1) i
x3: itree' E (X2 +ᵢ Y2) i
s1: it_eat i (observe (f i x1)) x0
s2: it_eat i (observe (g i x2)) x3
ss: it_eqF E (sumᵣ RX RY) (it_wbisim (sumᵣ RX RY)) i x0 x3

it_wbisim_t E RY R i (iter f i x1) (iter g i x2)
now apply CIH.
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2

it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2
it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2
it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2

it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2
it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inr y1))) ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
y1: Y1 i
r1: it_eat i (_observe (f i a)) (RetF (inr y1))
y2: Y2 i
r2: it_eat i (_observe (g i b)) (RetF (inr y2))
H0: RY i y1 y2

it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Ret' (inr y1))) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Ret' (inr y2)))
now cbn; econstructor.
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2

it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2
it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2
it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2

it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2
it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Tau' t1)) ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2

it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Tau' t1)) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Tau' t2))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2

it_wbisim_t E RY R i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2

it_wbisim_t E RY (it_wbisim_t E RY R) i ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t1) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t2)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
t1: itree E (X1 +ᵢ Y1) i
r1: it_eat i (_observe (f i a)) (TauF t1)
t2: itree E (X2 +ᵢ Y2) i
r2: it_eat i (_observe (g i b)) (TauF t2)
t_rel: it_wbisim (sumᵣ RX RY) i t1 t2

forall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_wbisim_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}
intros ? ? ? []; apply (tt_t (it_wbisim_map E RY)), (b_t (it_wbisim_map E RY)); cbn; eauto.
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)

it_wbisimF E RY (it_wbisim_t E RY R) i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)

it_eat i match _observe (f i a) with | RetF (inl x) => TauF (iter f i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X1 +ᵢ Y1) i) => {| _observe := match r0 with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k r) end ?x1
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
it_eqF E RY (it_wbisim_t E RY R) i ?x1 ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)

it_eat i match _observe (g i b) with | RetF (inl x) => TauF (iter g i x) | RetF (inr y) => RetF y | TauF t => TauF ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< t) | VisF e k => VisF e (fun r : e_rsp e => (fun (i : I) (r0 : (X2 +ᵢ Y2) i) => {| _observe := match r0 with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k r) end ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Vis' q k1)) ?x2
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)

it_eqF E RY (it_wbisim_t E RY R) i (_observe ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< Vis' q k1)) (_observe ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< Vis' q k2))
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
r0: e_rsp q

it_wbisim_t E RY R (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
r0: e_rsp q

it_wbisim_t E RY (it_wbisim_t E RY R) (e_nxt r0) ((fun (i : I) (r : (X1 +ᵢ Y1) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}) =<< k1 r0) ((fun (i : I) (r : (X2 +ᵢ Y2) i) => {| _observe := match r with | inl x => TauF (iter g i x) | inr y => RetF y end |}) =<< k2 r0)
I: Type
E: event I I
X1, X2, Y1, Y2: psh I
RX: relᵢ X1 X2
RY: relᵢ Y1 Y2
f: forall x : I, X1 x -> itree E (X1 +ᵢ Y1) x
g: forall x : I, X2 x -> itree E (X2 +ᵢ Y2) x
H: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim (sumᵣ RX RY) i (f i a) (g i b)
R: relᵢ (itree E Y1) (itree E Y2)
CIH: forall (i : I) (a : X1 i) (b : X2 i), RX i a b -> it_wbisim_t E RY R i (iter f i a) (iter g i b)
i: I
a: X1 i
b: X2 i
r: RX i a b
q: e_qry i
k1: forall x : e_rsp q, itree E (X1 +ᵢ Y1) (e_nxt x)
r1: it_eat i (_observe (f i a)) (VisF q k1)
k2: forall x : e_rsp q, itree E (X2 +ᵢ Y2) (e_nxt x)
r2: it_eat i (_observe (g i b)) (VisF q k2)
k_rel: forall r : e_rsp q, it_wbisim (sumᵣ RX RY) (e_nxt r) (k1 r) (k2 r)
r0: e_rsp q

forall (i : I) (x1 : (X1 +ᵢ Y1) i) (x2 : (X2 +ᵢ Y2) i), sumᵣ RX RY i x1 x2 -> it_wbisim_t E RY R i {| _observe := match x1 with | inl x => TauF (iter f i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter g i x) | inr y => RetF y end |}
intros ? ? ? []; apply (tt_t (it_wbisim_map E RY)), (b_t (it_wbisim_map E RY)); cbn; eauto. Qed. #[global] Instance iter_weq {X Y} {RX : relᵢ X X} {RY : relᵢ Y Y} : Proper (dpointwise_relation (fun i => RX i ==> it_wbisim (sumᵣ RX RY) i) ==> dpointwise_relation (fun i => RX i ==> it_wbisim RY i)) (@iter I E X Y) := iter_cong_weak.

Iteration is a strong fixed point of the folowing guarded equation.

  
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X i

it_eq RY (iter f i x) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X i

it_eq RY (iter f i x) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X i

it_eq_map E RY (gfp (it_eq_map E RY)) i (iter f i x) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Reflexiveᵢ0: Reflexiveᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
i: I
x: X i
r: (X +ᵢ Y) i

it_eqF E RY (gfp (it_eq_map E RY)) i match r with | inl x => TauF (iter f i x) | inr y => RetF y end match r with | inl x => TauF (iter f i x) | inr y => RetF y end
destruct r; eauto. Qed.

Iteration is the unique such fixed point w.r.t. strong bisimilarity. Note that this is again not w.r.t. the initial equation but the alternate one which is trivially guarded. See example 6.14 in the paper.

  
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))

forall (i : I) (x : X i), it_eq RY (g i x) (iter f i x)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))

forall (i : I) (x : X i), it_eq RY (g i x) (iter f i x)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

it_eq_bt E RY R i (g i x) (iter f i x)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

(it_eq_t E RY ° it_eq_bt E RY) R i (g i x) (iter f i x)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

(it_eq_t E RY ° it_eq_bt E RY) R i (g i x) ?y
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
(it_eq_t E RY ° it_eq_bt E RY) R i ?y (iter f i x)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

(it_eq_t E RY ° it_eq_bt E RY) R i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) (iter f i x)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

(it_eq_t E RY ° it_eq_bt E RY) R i ?y (iter f i x)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
(it_eq_t E RY ° it_eq_bt E RY) R i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) ?y
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

(it_eq_t E RY ° it_eq_bt E RY) R i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

bindR_eq_map (eqᵢ (X +ᵢ Y)) (it_eq_bt E RY R) i (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (g i x) | inr y => RetF y end |})) (f i x >>= (fun (i : I) (r : (X +ᵢ Y) i) => {| _observe := match r with | inl x => TauF (iter f i x) | inr y => RetF y end |}))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

f i x ≊ f i x
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
forall (i : I) (x1 x2 : (X +ᵢ Y) i), eqᵢ (X +ᵢ Y) i x1 x2 -> it_eq_bt E RY R i {| _observe := match x1 with | inl x => TauF (g i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter f i x) | inr y => RetF y end |}
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i

forall (i : I) (x1 x2 : (X +ᵢ Y) i), eqᵢ (X +ᵢ Y) i x1 x2 -> it_eq_bt E RY R i {| _observe := match x1 with | inl x => TauF (g i x) | inr y => RetF y end |} {| _observe := match x2 with | inl x => TauF (iter f i x) | inr y => RetF y end |}
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
i0: I
x0: X i0

it_eq_t E RY R i0 (g i0 x0) (iter f i0 x0)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
i0: I
y: Y i0
RY i0 y y
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
Equivalenceᵢ0: Equivalenceᵢ RY
f: X ⇒ᵢ itree E (X +ᵢ Y)
g: X ⇒ᵢ itree E Y
EQ: forall (i : I) (x : X i), it_eq RY (g i x) (f i x >>= (fun (i0 : I) (r : (X +ᵢ Y) i0) => {| _observe := match r with | inl x0 => TauF (g i0 x0) | inr y => RetF y end |}))
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i), it_eq_t E RY R i (g i x) (iter f i x)
i: I
x: X i
i0: I
y: Y i0

RY i0 y y
reflexivity. Qed. End withE.

Misc. utilities.

Variant is_tau' {I} {E : event I I} {X i} : itree' E X i -> Prop :=
  | IsTau {t : itree E X i} : is_tau' (TauF t) .
Definition is_tau {I} {E : event I I} {X i} (t : itree E X i) : Prop := is_tau' t.(_observe).

Variant is_ret' {I} {E : event I I} {X i} : itree' E X i -> Prop :=
  | IsRet {x : X i} : is_ret' (RetF x) .
Definition is_ret {I} {E : event I I} {X i} (t : itree E X i) : Prop := is_ret' t.(_observe).

I: Type
E: event I I
X: psh I
i: I
t: itree E X i

is_ret t -> X i
I: Type
E: event I I
X: psh I
i: I
t: itree E X i

is_ret t -> X i
I: Type
E: event I I
X: psh I
i: I
t: itree E X i

is_ret' (_observe t) -> X i
I: Type
E: event I I
X: psh I
i: I
t: itree E X i
r: X i
p: is_ret' (RetF r)

X i
exact r. Defined.