Guarded Iteration

The iter combinator, adapted directly from the Interaction Tree library, happily builds a computation iter f for any set of equations f. The resulting computation satisfies in particular an unfolding equation: iter f i ≈ f i >>= case_ (iter f) (ret) In general, this solution is however not unique, depriving us from a powerful tool to prove the equivalence of two computations.

Through this file, we recover uniqueness by introducing an alternate combinator iter_guarded restricted to so-called guarded sets of equations: they cannot be reduced to immediately returning a new index to iterate over. Both combinators agree over guarded equations, but the new one satisfies uniqueness.

Then, we refine the result to allow more sets of equations: not all must be guarded, but they must always finitely lead to a guarded one.

Guarded iteration

Section guarded.

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

A set of equations is an (indexed) family of computations, i.e. body fed to the combinator.

  Definition eqn R X Y : Type := X ⇒ᵢ itree E (Y +ᵢ R) .

  Definition apply_eqn {R X Y} (q : eqn R X Y) : itree E (X +ᵢ R) ⇒ᵢ itree E (Y +ᵢ R) :=
    fun _ t => t >>= fun _ r => match r with
                            | inl x => q _ x
                            | inr y => Ret' (inr y)
                            end .

A computation is guarded if it is not reduced to Ret (inl i), i.e. if as part of the loop, this specific iteration will be observable w.r.t. strong bisimilarity. It therefore may:

end the iteration
produce a silent step
produce an external event

A set of equation is then said to be guarded if all its equations are guarded.

  Variant guarded' {X Y i} : itree' E (X +ᵢ Y) i -> Prop :=
    | GRet y : guarded' (RetF (inr y))
    | GTau t : guarded' (TauF t)
    | GVis e k : guarded' (VisF e k)
  .
  Definition guarded {X Y i} (t : itree E (X +ᵢ Y) i)
    := guarded' t.(_observe).
  Definition eqn_guarded {R X Y} (e : eqn R X Y) : Prop
    := forall i (x : X i), guarded (e i x) .

The iter combinator gets away with putting no restriction on the equations by aggressively guarding with Tau all recursive calls. In contrast, by assuming the equations are guarded, we do not need to introduce any spurious guard: they are only legitimate in the case of returning immediately a new index, which we can here rule out via elim_guarded.

  Equations elim_guarded {R X i x} : @guarded' R X i (RetF (inl x)) -> T0 := | ! .

  Definition iter_guarded_aux {R X}
    (e : eqn R X X) (EG : eqn_guarded e)
    : itree E (X +ᵢ R) ⇒ᵢ itree E R
    := cofix CIH i t :=
      t >>= fun _ r =>
          go match r with
            | inl x => match (e _ x).(_observe) as t return guarded' t -> _ with
                      | RetF (inl x) => fun g => ex_falso (elim_guarded g)
                      | RetF (inr r) => fun _ => RetF r
                      | TauF t       => fun _ => TauF (CIH _ t)
                      | VisF q k     => fun _ => VisF q (fun r => CIH _ (k r))
                      end (EG _ x)
            | inr y => RetF y
            end .

  Definition iter_guarded {R X}
    (f : eqn R X X) (EG : eqn_guarded f)
    : X ⇒ᵢ itree E R
    := fun _ x =>
      go (match (f _ x).(_observe) as t return guarded' t -> _ with
          | RetF (inl x) => fun g => ex_falso (elim_guarded g)
          | RetF (inr r) => fun _ => RetF r
          | TauF t       => fun _ => TauF (iter_guarded_aux f EG _ t)
          | VisF q k     => fun _ => VisF q (fun r => iter_guarded_aux f EG _ (k r))
          end (EG _ x)) .

The absence of a spurious guard is reflected in the unfolding equation: w.r.t. strong bisimilarity, it directly satisfies what one would expect, i.e. we run the current equation, and either terminate or jump to the next one.

  Lemma iter_guarded_aux_unfold {X Y RY} {_ : Reflexiveᵢ RY}
    (f : eqn Y X X) (EG : eqn_guarded f) {i} (t : itree E (X +ᵢ Y) i)
    : it_eq RY
      (iter_guarded_aux f EG i t)
      (t >>= fun _ r => match r with
                     | inl x => iter_guarded f EG _ x
                     | inr y => Ret' y
                     end).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
i: I
t: itree E (X +ᵢ Y) i
it_eq RY (iter_guarded_aux f EG i t)
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
  Proof.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
i: I
t: itree E (X +ᵢ Y) i
it_eq RY (iter_guarded_aux f EG i t)
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
    revert i t; unfold it_eq; coinduction R CIH; intros i t.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
it_eq_bt E RY R i (iter_guarded_aux f EG i t)
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
    cbn; pose (ot := _observe t); fold ot.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
ot:= _observe t: itree' E (X +ᵢ Y) i
it_eqF E RY (it_eq_t E RY R) i
  match ot with
  | RetF (inl x) =>
      match
        _observe (f i x) as t
        return (guarded' t -> itree' E Y i)
      with
      | RetF r0 =>
          match
            r0 as r1
            return
              (guarded' (RetF r1) -> itree' E Y i)
          with
          | inl x0 => ex_falso ∘ elim_guarded
          | inr r1 =>
              fun _ : guarded' (RetF (inr r1)) =>
              RetF r1
          end
      | TauF t =>
          fun _ : guarded' (TauF t) =>
          TauF (iter_guarded_aux f EG i t)
      | VisF q k =>
          fun _ : guarded' (VisF q k) =>
          VisF q
            (fun r0 : e_rsp q =>
             iter_guarded_aux f EG (e_nxt r0) (k r0))
      end (EG i x)
  | RetF (inr y) => RetF y
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          {|
            _observe :=
              match r with
              | inl x =>
                  match
                    _observe (f i x) as t0
                    return
                      (guarded' t0 -> itree' E Y i)
                  with
                  | RetF r0 =>
                      match
                        r0 as r1
                        return
                          (guarded' (RetF r1) ->
                           itree' E Y i)
                      with
                      | inl x0 =>
                          ex_falso ∘ elim_guarded
                      | inr r1 =>
                          fun
                            _ : guarded'
                                  (RetF (inr r1)) =>
                          RetF r1
                      end
                  | TauF t0 =>
                      fun _ : guarded' (TauF t0) =>
                      TauF
                        (iter_guarded_aux f EG i t0)
                  | VisF q k =>
                      fun _ : guarded' (VisF q k) =>
                      VisF q
                        (fun r0 : e_rsp q =>
                         iter_guarded_aux f EG
                           (e_nxt r0) (k r0))
                  end (EG i x)
              | inr y => RetF y
              end
          |}) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          {|
            _observe :=
              match r0 with
              | inl x =>
                  match
                    _observe (f i x) as t
                    return
                      (guarded' t -> itree' E Y i)
                  with
                  | RetF r1 =>
                      match
                        r1 as r2
                        return
                          (guarded' (RetF r2) ->
                           itree' E Y i)
                      with
                      | inl x0 =>
                          ex_falso ∘ elim_guarded
                      | inr r2 =>
                          fun
                            _ : guarded'
                                  (RetF (inr r2)) =>
                          RetF r2
                      end
                  | TauF t =>
                      fun _ : guarded' (TauF t) =>
                      TauF (iter_guarded_aux f EG i t)
                  | VisF q k0 =>
                      fun _ : guarded' (VisF q k0) =>
                      VisF q
                        (fun r1 : e_rsp q =>
                         iter_guarded_aux f EG
                           (e_nxt r1) (k0 r1))
                  end (EG i x)
              | inr y => RetF y
              end
          |}) =<< k r)
  end
  match ot with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    destruct ot as [ [] | | ]; cbn.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
x: X i
it_eqF E RY (it_eq_t E RY R) i
  (match
     _observe (f i x) as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF (iter_guarded_aux f EG i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux f EG (e_nxt r) (k r))
   end (EG i x))
  (match
     _observe (f i x) as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF (iter_guarded_aux f EG i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux f EG (e_nxt r) (k r))
   end (EG i x))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
y: Y i
it_eqF E RY (it_eq_t E RY R) i (RetF y) (RetF y)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t, t0: itree E (X +ᵢ Y) i
it_eqF E RY (it_eq_t E RY R) i
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r with
           | inl x =>
               match
                 _observe (f i x) as t
                 return (guarded' t -> itree' E Y i)
               with
               | RetF r0 =>
                   match
                     r0 as r1
                     return
                       (guarded' (RetF r1) ->
                        itree' E Y i)
                   with
                   | inl x0 => ex_falso ∘ elim_guarded
                   | inr r1 =>
                       fun
                         _ : guarded' (RetF (inr r1))
                       => RetF r1
                   end
               | TauF t =>
                   fun _ : guarded' (TauF t) =>
                   TauF (iter_guarded_aux f EG i t)
               | VisF q k =>
                   fun _ : guarded' (VisF q k) =>
                   VisF q
                     (fun r0 : e_rsp q =>
                      iter_guarded_aux f EG (e_nxt r0)
                        (k r0))
               end (EG i x)
           | inr y => RetF y
           end
       |}) =<< t0))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< t0))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
it_eqF E RY (it_eq_t E RY R) i
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r0 with
           | inl x =>
               match
                 _observe (f i x) as t
                 return (guarded' t -> itree' E Y i)
               with
               | RetF r1 =>
                   match
                     r1 as r2
                     return
                       (guarded' (RetF r2) ->
                        itree' E Y i)
                   with
                   | inl x0 => ex_falso ∘ elim_guarded
                   | inr r2 =>
                       fun
                         _ : guarded' (RetF (inr r2))
                       => RetF r2
                   end
               | TauF t =>
                   fun _ : guarded' (TauF t) =>
                   TauF (iter_guarded_aux f EG i t)
               | VisF q k =>
                   fun _ : guarded' (VisF q k) =>
                   VisF q
                     (fun r1 : e_rsp q =>
                      iter_guarded_aux f EG (e_nxt r1)
                        (k r1))
               end (EG i x)
           | inr y => RetF y
           end
       |}) =<< k r))
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
    1: destruct (EG i x).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
x: X i
y: Y i
it_eqF E RY (it_eq_t E RY R) i (RetF y) (RetF y)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
x: X i
t0: itree E (X +ᵢ Y) i
it_eqF E RY (it_eq_t E RY R) i
  (TauF (iter_guarded_aux f EG i t0))
  (TauF (iter_guarded_aux f EG i t0))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
it_eqF E RY (it_eq_t E RY R) i
  (VisF e
     (fun r : e_rsp e =>
      iter_guarded_aux f EG (e_nxt r) (k r)))
  (VisF e
     (fun r : e_rsp e =>
      iter_guarded_aux f EG (e_nxt r) (k r)))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
y: Y i
it_eqF E RY (it_eq_t E RY R) i (RetF y) (RetF y)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t, t0: itree E (X +ᵢ Y) i
it_eqF E RY (it_eq_t E RY R) i
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r with
           | inl x =>
               match
                 _observe (f i x) as t
                 return (guarded' t -> itree' E Y i)
               with
               | RetF r0 =>
                   match
                     r0 as r1
                     return
                       (guarded' (RetF r1) ->
                        itree' E Y i)
                   with
                   | inl x0 => ex_falso ∘ elim_guarded
                   | inr r1 =>
                       fun
                         _ : guarded' (RetF (inr r1))
                       => RetF r1
                   end
               | TauF t =>
                   fun _ : guarded' (TauF t) =>
                   TauF (iter_guarded_aux f EG i t)
               | VisF q k =>
                   fun _ : guarded' (VisF q k) =>
                   VisF q
                     (fun r0 : e_rsp q =>
                      iter_guarded_aux f EG (e_nxt r0)
                        (k r0))
               end (EG i x)
           | inr y => RetF y
           end
       |}) =<< t0))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< t0))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
it_eqF E RY (it_eq_t E RY R) i
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r0 with
           | inl x =>
               match
                 _observe (f i x) as t
                 return (guarded' t -> itree' E Y i)
               with
               | RetF r1 =>
                   match
                     r1 as r2
                     return
                       (guarded' (RetF r2) ->
                        itree' E Y i)
                   with
                   | inl x0 => ex_falso ∘ elim_guarded
                   | inr r2 =>
                       fun
                         _ : guarded' (RetF (inr r2))
                       => RetF r2
                   end
               | TauF t =>
                   fun _ : guarded' (TauF t) =>
                   TauF (iter_guarded_aux f EG i t)
               | VisF q k =>
                   fun _ : guarded' (VisF q k) =>
                   VisF q
                     (fun r1 : e_rsp q =>
                      iter_guarded_aux f EG (e_nxt r1)
                        (k r1))
               end (EG i x)
           | inr y => RetF y
           end
       |}) =<< k r))
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
    all: econstructor; auto.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t, t0: itree E (X +ᵢ Y) i
it_eq_t E RY R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x =>
            match
              _observe (f i x) as t
              return (guarded' t -> itree' E Y i)
            with
            | RetF r0 =>
                match
                  r0 as r1
                  return
                    (guarded' (RetF r1) ->
                     itree' E Y i)
                with
                | inl x0 => ex_falso ∘ elim_guarded
                | inr r1 =>
                    fun _ : guarded' (RetF (inr r1))
                    => RetF r1
                end
            | TauF t =>
                fun _ : guarded' (TauF t) =>
                TauF (iter_guarded_aux f EG i t)
            | VisF q k =>
                fun _ : guarded' (VisF q k) =>
                VisF q
                  (fun r0 : e_rsp q =>
                   iter_guarded_aux f EG (e_nxt r0)
                     (k r0))
            end (EG i x)
        | inr y => RetF y
        end
    |}) =<< t0)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< t0)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
forall r : e_rsp q,
it_eq_t E RY R (e_nxt r)
  ((fun (i : I) (r0 : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r0 with
        | inl x =>
            match
              _observe (f i x) as t
              return (guarded' t -> itree' E Y i)
            with
            | RetF r1 =>
                match
                  r1 as r2
                  return
                    (guarded' (RetF r2) ->
                     itree' E Y i)
                with
                | inl x0 => ex_falso ∘ elim_guarded
                | inr r2 =>
                    fun _ : guarded' (RetF (inr r2))
                    => RetF r2
                end
            | TauF t =>
                fun _ : guarded' (TauF t) =>
                TauF (iter_guarded_aux f EG i t)
            | VisF q k =>
                fun _ : guarded' (VisF q k) =>
                VisF q
                  (fun r1 : e_rsp q =>
                   iter_guarded_aux f EG (e_nxt r1)
                     (k r1))
            end (EG i x)
        | inr y => RetF y
        end
    |}) =<< k r)
  ((fun (i : I) (r0 : (X +ᵢ Y) i) =>
    match r0 with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
    2: intro r.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t, t0: itree E (X +ᵢ Y) i
it_eq_t E RY R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x =>
            match
              _observe (f i x) as t
              return (guarded' t -> itree' E Y i)
            with
            | RetF r0 =>
                match
                  r0 as r1
                  return
                    (guarded' (RetF r1) ->
                     itree' E Y i)
                with
                | inl x0 => ex_falso ∘ elim_guarded
                | inr r1 =>
                    fun _ : guarded' (RetF (inr r1))
                    => RetF r1
                end
            | TauF t =>
                fun _ : guarded' (TauF t) =>
                TauF (iter_guarded_aux f EG i t)
            | VisF q k =>
                fun _ : guarded' (VisF q k) =>
                VisF q
                  (fun r0 : e_rsp q =>
                   iter_guarded_aux f EG (e_nxt r0)
                     (k r0))
            end (EG i x)
        | inr y => RetF y
        end
    |}) =<< t0)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< t0)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
r: e_rsp q
it_eq_t E RY R (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x =>
            match
              _observe (f i x) as t
              return (guarded' t -> itree' E Y i)
            with
            | RetF r0 =>
                match
                  r0 as r1
                  return
                    (guarded' (RetF r1) ->
                     itree' E Y i)
                with
                | inl x0 => ex_falso ∘ elim_guarded
                | inr r1 =>
                    fun _ : guarded' (RetF (inr r1))
                    => RetF r1
                end
            | TauF t =>
                fun _ : guarded' (TauF t) =>
                TauF (iter_guarded_aux f EG i t)
            | VisF q k =>
                fun _ : guarded' (VisF q k) =>
                VisF q
                  (fun r0 : e_rsp q =>
                   iter_guarded_aux f EG (e_nxt r0)
                     (k r0))
            end (EG i x)
        | inr y => RetF y
        end
    |}) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
    all: apply (tt_t (it_eq_map E RY)); cbn; eapply it_eq_up2bind_t; econstructor; auto.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t, t0: itree E (X +ᵢ Y) i
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_eq_t E RY R i
  {|
    _observe :=
      match x1 with
      | inl x =>
          match
            _observe (f i x) as t
            return (guarded' t -> itree' E Y i)
          with
          | RetF r0 =>
              match
                r0 as r1
                return
                  (guarded' (RetF r1) -> itree' E Y i)
              with
              | inl x0 => ex_falso ∘ elim_guarded
              | inr r =>
                  fun _ : guarded' (RetF (inr r)) =>
                  RetF r
              end
          | TauF t =>
              fun _ : guarded' (TauF t) =>
              TauF (iter_guarded_aux f EG i t)
          | VisF q k =>
              fun _ : guarded' (VisF q k) =>
              VisF q
                (fun r : e_rsp q =>
                 iter_guarded_aux f EG (e_nxt r) (k r))
          end (EG i x)
      | inr y => RetF y
      end
  |}
  match x2 with
  | inl x => iter_guarded f EG i x
  | inr y => Ret' y
  end
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (t0 : itree E (X +ᵢ Y) i),
it_eq_t E RY R i (iter_guarded_aux f EG i t0)
(t0 >>=
(fun (i0 : I) (r : (X +ᵢ Y) i0) =>
match r with
| inl x => iter_guarded f EG i0 x
| inr y => Ret' y
end))
i: I
t: itree E (X +ᵢ Y) i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
r: e_rsp q
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_eq_t E RY R i
  {|
    _observe :=
      match x1 with
      | inl x =>
          match
            _observe (f i x) as t
            return (guarded' t -> itree' E Y i)
          with
          | RetF r0 =>
              match
                r0 as r1
                return
                  (guarded' (RetF r1) -> itree' E Y i)
              with
              | inl x0 => ex_falso ∘ elim_guarded
              | inr r =>
                  fun _ : guarded' (RetF (inr r)) =>
                  RetF r
              end
          | TauF t =>
              fun _ : guarded' (TauF t) =>
              TauF (iter_guarded_aux f EG i t)
          | VisF q k =>
              fun _ : guarded' (VisF q k) =>
              VisF q
                (fun r : e_rsp q =>
                 iter_guarded_aux f EG (e_nxt r) (k r))
          end (EG i x)
      | inr y => RetF y
      end
  |}
  match x2 with
  | inl x => iter_guarded f EG i x
  | inr y => Ret' y
  end
    all: intros ? ? x2 ->; destruct x2; auto.
  Qed.

  Lemma iter_guarded_unfold {X Y RY} {_ : Reflexiveᵢ RY}
    (f : eqn Y X X) (EG : eqn_guarded f) {i x}
    : it_eq RY
      (iter_guarded f EG i x)
      (f i x >>= fun _ r => match r with
                         | inl x => iter_guarded f EG _ x
                         | inr y => Ret' y
                         end).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
i: I
x: X i
it_eq RY (iter_guarded f EG i x)
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
  Proof.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
i: I
x: X i
it_eq RY (iter_guarded f EG i x)
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
    apply it_eq_unstep; cbn.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
i: I
x: X i
it_eqF E RY (it_eq RY) i
  (match
     _observe (f i x) as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF (iter_guarded_aux f EG i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux f EG (e_nxt r) (k r))
   end (EG i x))
  match _observe (f i x) with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    pose (p := EG i x); fold p; unfold guarded in p.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
i: I
x: X i
p:= EG i x: guarded' (_observe (f i x))
it_eqF E RY (it_eq RY) i
  (match
     _observe (f i x) as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF (iter_guarded_aux f EG i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux f EG (e_nxt r) (k r))
   end p)
  match _observe (f i x) with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    pose (ot := _observe (f i x)); fold ot in p |- *.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Reflexiveᵢ RY
f: eqn Y X X
EG: eqn_guarded f
i: I
x: X i
ot:= _observe (f i x): itree' E (X +ᵢ Y) i
p:= EG i x: guarded' ot
it_eqF E RY (it_eq RY) i
  (match
     ot as t return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF (iter_guarded_aux f EG i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux f EG (e_nxt r) (k r))
   end p)
  match ot with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    destruct p; econstructor; [ now apply H | | intro r ]; apply iter_guarded_aux_unfold.
  Qed.

The payoff: iter_guarded does not only deliver a solution to the equations, but it also is unique.

  Lemma iter_guarded_uniq {X Y RY} {_ : Equivalenceᵢ RY}
    (f : eqn Y X X) (g : X ⇒ᵢ itree E Y)
    (EG : eqn_guarded f)
    (EQ : forall i x, it_eq RY
                   (g i x)
                   (bind (f i x) (fun _ r => match r with
                                          | inl x => g _ x
                                          | inr y => Ret' y end)))
    : forall i x, it_eq RY (g i x) (iter_guarded f EG i x).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' y
    end))
forall (i : I) (x : X i),
it_eq RY (g i x) (iter_guarded f EG i x)
  Proof.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' y
    end))
forall (i : I) (x : X i),
it_eq RY (g i x) (iter_guarded f EG i x)
    unfold it_eq; coinduction R CIH; intros i x.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
it_eq_bt E RY R i (g i x) (iter_guarded f EG i x)
    etransitivity; [ | symmetry; apply it_eq_t_bt, (iter_guarded_unfold f EG) ].I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
it_eq_bt E RY R i (g i x)
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
    rewrite (EQ i x); cbn.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
it_eqF E RY (it_eq_t E RY R) i
  match _observe (f i x) with
  | RetF r =>
      _observe
        match r with
        | inl x => g i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => g i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => g i x
          | inr y => Ret' y
          end) =<< k r)
  end
  match _observe (f i x) with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    pose (a := (f i x).(_observe)); fold a.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
a:= _observe (f i x): itree' E (X +ᵢ Y) i
it_eqF E RY (it_eq_t E RY R) i
  match a with
  | RetF r =>
      _observe
        match r with
        | inl x => g i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => g i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => g i x
          | inr y => Ret' y
          end) =<< k r)
  end
  match a with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    pose (Ha := EG i x); unfold guarded in Ha; fold a in Ha.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
a:= _observe (f i x): itree' E (X +ᵢ Y) i
Ha:= EG i x: guarded' a
it_eqF E RY (it_eq_t E RY R) i
  match a with
  | RetF r =>
      _observe
        match r with
        | inl x => g i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => g i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => g i x
          | inr y => Ret' y
          end) =<< k r)
  end
  match a with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    destruct Ha; cbn; econstructor; auto; [ | intro r ].I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
it_eq_t E RY R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end) =<< t)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< t)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
r: e_rsp e
it_eq_t E RY R (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
    all: change (subst ?f _ ?t) with (bind t f).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
it_eq_t E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
r: e_rsp e
it_eq_t E RY R (e_nxt r)
  (k r >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (k r >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
    all: eapply (tt_t (it_eq_map E RY)).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
(it_eq_t E RY ° it_eq_t E RY) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
r: e_rsp e
(it_eq_t E RY ° it_eq_t E RY) R (e_nxt r)
  (k r >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (k r >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
    all: refine (it_eq_up2bind_t _ _ _ _ _ _ _); econstructor; eauto.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_eq_t E RY R i
  match x1 with
  | inl x => g i x
  | inr y => Ret' y
  end
  match x2 with
  | inl x => iter_guarded f EG i x
  | inr y => Ret' y
  end
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_guarded f EG i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
r: e_rsp e
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_eq_t E RY R i
  match x1 with
  | inl x => g i x
  | inr y => Ret' y
  end
  match x2 with
  | inl x => iter_guarded f EG i x
  | inr y => Ret' y
  end
    all: intros ? ? ? <-; destruct x1; auto.
  Qed.

Furthermore, w.r.t. weak bisimilarity, we compute the same solution as what iter does.

  Lemma guarded_cong' {X Y} {i}
    (s t : itree' E (X +ᵢ Y) i) (EQ : it_eq' (eqᵢ _) s t)
    (g : guarded' s) : guarded' t.I: Type
E: event I I
X, Y: psh I
i: I
s, t: itree' E (X +ᵢ Y) i
EQ: it_eq' (eqᵢ (X +ᵢ Y)) s t
g: guarded' s
guarded' t
  Proof.I: Type
E: event I I
X, Y: psh I
i: I
s, t: itree' E (X +ᵢ Y) i
EQ: it_eq' (eqᵢ (X +ᵢ Y)) s t
g: guarded' s
guarded' t
    destruct EQ as [ [] | | ]; [ dependent elimination g | rewrite <- r_rel | | ]; econstructor.
  Qed.

  Definition guarded_cong {X Y} {i} (s t : itree E (X +ᵢ Y) i)
    (EQ : s ≊ t) (g : guarded s) : guarded t
    := guarded_cong' s.(_observe) t.(_observe) (it_eq_step _ _ _ EQ) g .

  Lemma iter_guarded_iter {X Y}
    (f : eqn Y X X) (EG : eqn_guarded f) {i x}
    : iter_guarded f EG i x ≈ iter f i x .I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
i: I
x: X i
iter_guarded f EG i x ≈ iter f i x
  Proof.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
i: I
x: X i
iter_guarded f EG i x ≈ iter f i x
    revert i x; unfold it_wbisim; coinduction R CIH; intros i x.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i (iter_guarded f EG i x)
  (iter f i x)
    eapply (@fbt_bt _ _ (it_wbisim_map E (eqᵢ Y)) _ it_wbisim_up2eq).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
(eq_clo_map ° it_wbisim_bt E (eqᵢ Y)) R i
  (iter_guarded f EG i x) (iter f i x)
    econstructor.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
iter_guarded f EG i x ≊ ?a
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
?b ≊ iter f i x
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i ?a ?b
    apply iter_guarded_unfold.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
?b ≊ iter f i x
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end)) ?b
    symmetry; apply iter_unfold.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' 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
    |}))
    remember (EG _ x) as g; clear Heqg.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
g: guarded (f i x)
it_wbisim_bt E (eqᵢ Y) R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' 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
    |}))
    remember (f i x) as t; clear Heqt.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
g: guarded t
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
    unfold guarded in g.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
g: guarded' (_observe t)
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
    remember (_observe t) as ot.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
ot: itree' E (X +ᵢ Y) i
Heqot: ot = _observe t
g: guarded' ot
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
    destruct g; cbn ; rewrite <- Heqot; cbn.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
y: Y i
Heqot: RetF (inr y) = _observe t
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (RetF y) (RetF y)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, t0: itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< t0))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< t0))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
Heqot: VisF e k = _observe t
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r0 with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< k r))
    econstructor; auto.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, t0: itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< t0))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< t0))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
Heqot: VisF e k = _observe t
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r0 with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< k r))
    all: econstructor; auto; econstructor; intros.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, t0: itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t
it_wbisim_t E (eqᵢ Y) R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< t0)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< t0)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
Heqot: VisF e k = _observe t
r: e_rsp e
it_wbisim_t E (eqᵢ Y) R 
  (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< k r)
    all: eapply (tt_t (it_wbisim_map E (eqᵢ Y))).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, t0: itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< t0)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< t0)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
Heqot: VisF e k = _observe t
r: e_rsp e
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R
  (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< k r)
    all: refine (it_wbisim_up2bind_t _ _ _ _ _ _ _); econstructor; auto.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, t0: itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_wbisim_t E (eqᵢ Y) R i
  match x1 with
  | inl x => iter_guarded f EG i x
  | inr y => Ret' 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
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
Heqot: VisF e k = _observe t
r: e_rsp e
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_wbisim_t E (eqᵢ Y) R i
  match x1 with
  | inl x => iter_guarded f EG i x
  | inr y => Ret' y
  end
  {|
    _observe :=
      match x2 with
      | inl x => TauF (iter f i x)
      | inr y => RetF y
      end
  |}
    all: intros ? ? x2 ->; destruct x2; auto.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, t0: itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t
i0: I
x0: X i0
it_wbisim_t E (eqᵢ Y) R i0 
  (iter_guarded f EG i0 x0) 
  (Tau' (iter f i0 x0))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
Heqot: VisF e k = _observe t
r: e_rsp e
i0: I
x0: X i0
it_wbisim_t E (eqᵢ Y) R i0 
  (iter_guarded f EG i0 x0) 
  (Tau' (iter f i0 x0))
    all: eapply (tt_t (it_wbisim_map E (eqᵢ Y))).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, t0: itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t
i0: I
x0: X i0
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R i0
  (iter_guarded f EG i0 x0) 
  (Tau' (iter f i0 x0))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
Heqot: VisF e k = _observe t
r: e_rsp e
i0: I
x0: X i0
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R i0
  (iter_guarded f EG i0 x0) 
  (Tau' (iter f i0 x0))
    all: cbn; apply it_wbisim_up2eat; econstructor;
      [ exact EatRefl | exact (EatStep EatRefl) | apply CIH ].
  Qed.

Minor technical lemmas: guardedness is proof irrelevant.

  Lemma guarded'_irrelevant {R X i t} (p q : @guarded' R X i t) : p = q .I: Type
E: event I I
R, X: psh I
i: I
t: itree' E (R +ᵢ X) i
p, q: guarded' t
p = q
    destruct t; dependent elimination p; dependent elimination q; reflexivity.
  Qed.

  Lemma guarded_irrelevant {R X i t} (p q : @guarded R X i t) : p = q .I: Type
E: event I I
R, X: psh I
i: I
t: itree E (R +ᵢ X) i
p, q: guarded t
p = q
    apply guarded'_irrelevant.
  Qed.

End guarded.

Eventually guarded iteration

For our purpose, proving the soundness of the ogs, guardedness is a bit too restrictive: while not all equations are guarded, they all inductively lead to a guarded one. We capture this intuition via the notion of "eventually guarded" set of equations, and establish similar result to ones in the guarded case.

Section eventually_guarded.

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

A set of equations is eventually guarded if they all admit an inductive path following its non-guarded indirections that leads to a guarded equation.

  Unset Elimination Schemes.
  Inductive ev_guarded' {X Y} (e : eqn Y X X) {i} : itree' E (X +ᵢ Y) i -> Prop :=
  | GHead t : guarded' t -> ev_guarded' e t
  | GNext x : ev_guarded' e (e i x).(_observe) -> ev_guarded' e (RetF (inl x))
  .
  #[global] Arguments GHead {X Y e i t}.
  #[global] Arguments GNext {X Y e i x}.

  Scheme ev_guarded'_ind := Induction for ev_guarded' Sort Prop.
  Set Elimination Schemes.

  Definition ev_guarded {X Y} (e : eqn Y X X) {i} (t : itree E (X +ᵢ Y) i)
    := ev_guarded' e t.(_observe).
  Definition eqn_ev_guarded {X Y} (e : eqn Y X X) : Type
    := forall i (x : X i), ev_guarded e (e i x) .

  Equations elim_ev_guarded' {X Y e i x} (g : @ev_guarded' X Y e i (RetF (inl x)))
            : ev_guarded' e (e i x).(_observe) :=
    elim_ev_guarded' (GNext g) := g .

Given eventually guarded equations e, we can build a set of guarded equations eqn_evg_unroll_guarded e: we simply map all indices to their reachable guarded equations. Iteration over eventually guarded equations is hence defined as guarded iteration over their guarded counterpart.

  Fixpoint evg_unroll' {X Y} (e : eqn Y X X) {i}
    (t : itree' E (X +ᵢ Y) i) (g : ev_guarded' e t) { struct g } : itree' E (X +ᵢ Y) i
    := match t as t' return ev_guarded' e t' -> _ with
       | RetF (inl x) => fun g => evg_unroll' e (e _ x).(_observe) (elim_ev_guarded' g)
       | RetF (inr y) => fun _ => RetF (inr y)
       | TauF t       => fun _ => TauF t
       | VisF q k     => fun _ => VisF q k
       end g .

  Definition evg_unroll {X Y} (e : eqn Y X X) {i}
    (t : itree E (X +ᵢ Y) i) (g : ev_guarded e t) : itree E (X +ᵢ Y) i
    := go (evg_unroll' e t.(_observe) g) .

  Definition eqn_evg_unroll {X Y} (e : eqn Y X X) (H : eqn_ev_guarded e) : eqn Y X X
    := fun _ x => evg_unroll e _ (H _ x) .

  Lemma evg_unroll_guarded' {X Y} (e : eqn Y X X) {i}
    (t : itree' E (X +ᵢ Y) i) (g : ev_guarded' e t) : guarded' (evg_unroll' e t g).I: Type
E: event I I
X, Y: psh I
e: eqn Y X X
i: I
t: itree' E (X +ᵢ Y) i
g: ev_guarded' e t
guarded' (evg_unroll' e t g)
  Proof.I: Type
E: event I I
X, Y: psh I
e: eqn Y X X
i: I
t: itree' E (X +ᵢ Y) i
g: ev_guarded' e t
guarded' (evg_unroll' e t g)
    induction g; auto.I: Type
E: event I I
X, Y: psh I
e: eqn Y X X
i: I
t: itree' E (X +ᵢ Y) i
g: guarded' t
guarded' (evg_unroll' e t (GHead g))
    destruct t as [ [] | | ]; auto.I: Type
E: event I I
X, Y: psh I
e: eqn Y X X
i: I
x: X i
g: guarded' (RetF (inl x))
guarded' (evg_unroll' e (RetF (inl x)) (GHead g))
    dependent elimination g.
  Qed.

  Definition evg_unroll_guarded {X Y} (e : eqn Y X X) {i}
    (t : itree E (X +ᵢ Y) i) (EG : ev_guarded e t) : guarded (evg_unroll e t EG)
    := evg_unroll_guarded' e t.(_observe) EG.

  Definition eqn_evg_unroll_guarded {X Y}
    (e : eqn Y X X) (EG : eqn_ev_guarded e) : eqn_guarded (eqn_evg_unroll e EG)
    := fun _ x => evg_unroll_guarded e _ (EG _ x) .

  Definition iter_ev_guarded {R X}
    (e : eqn R X X) (EG : eqn_ev_guarded e) : X ⇒ᵢ itree E R
    := fun _ x => iter_guarded _ (eqn_evg_unroll_guarded e EG) _ x .

Once again, we establish the expected unfolding lemma, for eventually guarded iteration.

  Lemma evg_unroll'_equation {X Y}
    (e : eqn Y X X) {i} {x : X i} (g : ev_guarded' e (RetF (inl x)))
    : evg_unroll' e (RetF (inl x)) g = evg_unroll' e (e _ x).(_observe) (elim_ev_guarded' g) .I: Type
E: event I I
X, Y: psh I
e: eqn Y X X
i: I
x: X i
g: ev_guarded' e (RetF (inl x))
evg_unroll' e (RetF (inl x)) g =
evg_unroll' e (_observe (e i x)) (elim_ev_guarded' g)
  Proof.I: Type
E: event I I
X, Y: psh I
e: eqn Y X X
i: I
x: X i
g: ev_guarded' e (RetF (inl x))
evg_unroll' e (RetF (inl x)) g =
evg_unroll' e (_observe (e i x)) (elim_ev_guarded' g)
    dependent elimination g; [ dependent elimination g | reflexivity ] .
  Qed.

  Lemma ev_guarded'_irrelevant {R X e i t}
    (p q : @ev_guarded' R X e i t) : p = q .I: Type
E: event I I
R, X: psh I
e: eqn X R R
i: I
t: itree' E (R +ᵢ X) i
p, q: ev_guarded' e t
p = q
  Proof.I: Type
E: event I I
R, X: psh I
e: eqn X R R
i: I
t: itree' E (R +ᵢ X) i
p, q: ev_guarded' e t
p = q
    induction p.I: Type
E: event I I
R, X: psh I
e: eqn X R R
i: I
t: itree' E (R +ᵢ X) i
g: guarded' t
q: ev_guarded' e t
GHead g = q
I: Type
E: event I I
R, X: psh I
e: eqn X R R
i: I
x: R i
p: ev_guarded' e (_observe (e i x))
q: ev_guarded' e (RetF (inl x))
IHp: forall q : ev_guarded' e (_observe (e i x)), p = q
GNext p = q
    -I: Type
E: event I I
R, X: psh I
e: eqn X R R
i: I
t: itree' E (R +ᵢ X) i
g: guarded' t
q: ev_guarded' e t
GHead g = q destruct t as [ [] | | ]; [ dependent elimination g | | | ];
        dependent elimination q; f_equal; apply guarded'_irrelevant.
    -I: Type
E: event I I
R, X: psh I
e: eqn X R R
i: I
x: R i
p: ev_guarded' e (_observe (e i x))
q: ev_guarded' e (RetF (inl x))
IHp: forall q : ev_guarded' e (_observe (e i x)), p = q
GNext p = q dependent elimination q; [ dependent elimination g | ]; f_equal; apply IHp.
  Qed.

  Lemma iter_evg_unfold_lem {X Y RY} {_ : Equivalenceᵢ RY}
    (f : eqn Y X X) (EG : eqn_ev_guarded f) {i x1 x2}
    (p : (f i x1).(_observe) = RetF (inl x2))
    : it_eq RY
        (iter_ev_guarded f EG i x1)
        (iter_ev_guarded f EG i x2).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
p: _observe (f i x1) = RetF (inl x2)
it_eq RY (iter_ev_guarded f EG i x1)
  (iter_ev_guarded f EG i x2)
  Proof.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
p: _observe (f i x1) = RetF (inl x2)
it_eq RY (iter_ev_guarded f EG i x1)
  (iter_ev_guarded f EG i x2)
    unfold iter_ev_guarded at 1.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
p: _observe (f i x1) = RetF (inl x2)
it_eq RY
  (iter_guarded (eqn_evg_unroll f EG)
     (eqn_evg_unroll_guarded f EG) i x1)
  (iter_ev_guarded f EG i x2)
    etransitivity; [ apply iter_guarded_unfold | ].I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
p: _observe (f i x1) = RetF (inl x2)
it_eq RY
  (eqn_evg_unroll f EG i x1 >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x =>
        iter_guarded (eqn_evg_unroll f EG)
          (eqn_evg_unroll_guarded f EG) i x
    | inr y => Ret' y
    end)) (iter_ev_guarded f EG i x2)
    change (iter_guarded _ _ ?i ?x) with (iter_ev_guarded f EG i x).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
p: _observe (f i x1) = RetF (inl x2)
it_eq RY
  (eqn_evg_unroll f EG i x1 >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end)) (iter_ev_guarded f EG i x2)
    unfold eqn_evg_unroll; remember (EG i x1) as q; clear Heqq.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
p: _observe (f i x1) = RetF (inl x2)
q: ev_guarded f (f i x1)
it_eq RY
  (evg_unroll f (f i x1) q >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end)) (iter_ev_guarded f EG i x2)
    apply it_eq_unstep; unfold evg_unroll; cbn -[iter_ev_guarded].I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
p: _observe (f i x1) = RetF (inl x2)
q: ev_guarded f (f i x1)
it_eqF E RY (it_eq RY) i
  match evg_unroll' f (_observe (f i x1)) q with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_ev_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end (observe (iter_ev_guarded f EG i x2))
    unfold ev_guarded in q; revert q; rewrite p; clear p; intro q.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
q: ev_guarded' f (RetF (inl x2))
it_eqF E RY (it_eq RY) i
  match evg_unroll' f (RetF (inl x2)) q with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_ev_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end (observe (iter_ev_guarded f EG i x2))
    rewrite evg_unroll'_equation, (ev_guarded'_irrelevant (elim_ev_guarded' q) (EG _ x2)); clear q.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
it_eqF E RY (it_eq RY) i
  match
    evg_unroll' f (_observe (f i x2)) (EG i x2)
  with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_ev_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end (observe (iter_ev_guarded f EG i x2))
    change (it_eqF E RY (it_eq RY) i _ (observe ?a))
      with (it_eq_map E RY (it_eq RY) i
              (evg_unroll f (f i x2) (EG i x2) >>= fun (i0 : I) (r : (X +ᵢ Y) i0) =>
                   match r with
                   | inl x => iter_ev_guarded f EG i0 x
                   | inr y => Ret' y
                   end)
              a).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x1, x2: X i
it_eq_map E RY (it_eq RY) i
  (evg_unroll f (f i x2) (EG i x2) >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x => iter_ev_guarded f EG i0 x
    | inr y => Ret' y
    end)) (iter_ev_guarded f EG i x2)
    apply it_eq_step; symmetry; exact (iter_guarded_unfold _ _).
  Qed.

  Lemma iter_evg_unfold {X Y RY} {_ : Equivalenceᵢ RY}
    (f : eqn Y X X) (EG : eqn_ev_guarded f) {i x}
    : it_eq RY
        (iter_ev_guarded f EG i x)
        (f i x >>= fun _ r => match r with
                           | inl x => iter_ev_guarded f EG _ x
                           | inr y => Ret' y
                           end).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
it_eq RY (iter_ev_guarded f EG i x)
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  Proof.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
it_eq RY (iter_ev_guarded f EG i x)
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
    apply it_eq_unstep; cbn -[iter_ev_guarded].I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  match _observe (f i x) with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_ev_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    remember (EG i x) as g; clear Heqg; unfold ev_guarded in g.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
g: ev_guarded' f (_observe (f i x))
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  match _observe (f i x) with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_ev_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    remember (_observe (f i x)).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
i0: itree' E (X +ᵢ Y) i
Heqi0: i0 = _observe (f i x)
g: ev_guarded' f i0
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  match i0 with
  | RetF r =>
      _observe
        match r with
        | inl x => iter_ev_guarded f EG i x
        | inr y => Ret' y
        end
  | TauF t =>
      TauF
        ((fun (i : I) (r : (X +ᵢ Y) i) =>
          match r with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< t)
  | VisF e k =>
      VisF e
        (fun r : e_rsp e =>
         (fun (i : I) (r0 : (X +ᵢ Y) i) =>
          match r0 with
          | inl x => iter_ev_guarded f EG i x
          | inr y => Ret' y
          end) =<< k r)
  end
    destruct i0 as [ [] | | ].I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x, x0: X i
Heqi0: RetF (inl x0) = _observe (f i x)
g: ev_guarded' f (RetF (inl x0))
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  (_observe (iter_ev_guarded f EG i x0))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
y: Y i
Heqi0: RetF (inr y) = _observe (f i x)
g: ev_guarded' f (RetF (inr y))
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  (_observe (Ret' y))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
t: itree E (X +ᵢ Y) i
Heqi0: TauF t = _observe (f i x)
g: ev_guarded' f (TauF t)
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< t))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
Heqi0: VisF q k = _observe (f i x)
g: ev_guarded' f (VisF q k)
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
    apply (it_eq_step _ (iter_ev_guarded f EG i x) (iter_ev_guarded f EG i x0)), iter_evg_unfold_lem; auto.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
y: Y i
Heqi0: RetF (inr y) = _observe (f i x)
g: ev_guarded' f (RetF (inr y))
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  (_observe (Ret' y))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
t: itree E (X +ᵢ Y) i
Heqi0: TauF t = _observe (f i x)
g: ev_guarded' f (TauF t)
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< t))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
Heqi0: VisF q k = _observe (f i x)
g: ev_guarded' f (VisF q k)
it_eqF E RY (it_eq RY) i
  (observe (iter_ev_guarded f EG i x))
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
    all: clear g; cbn; unfold eqn_evg_unroll_guarded at 3, evg_unroll_guarded.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
y: Y i
Heqi0: RetF (inr y) = _observe (f i x)
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (_observe (f i x)) (EG i x) as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end
     (evg_unroll_guarded' f 
        (_observe (f i x)) 
        (EG i x))) (RetF y)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
t: itree E (X +ᵢ Y) i
Heqi0: TauF t = _observe (f i x)
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (_observe (f i x)) (EG i x) as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end
     (evg_unroll_guarded' f 
        (_observe (f i x)) 
        (EG i x)))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< t))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
Heqi0: VisF q k = _observe (f i x)
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (_observe (f i x)) (EG i x) as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end
     (evg_unroll_guarded' f 
        (_observe (f i x)) 
        (EG i x)))
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
    all: remember (EG i x) as g'; clear Heqg'; unfold ev_guarded in g'.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
y: Y i
Heqi0: RetF (inr y) = _observe (f i x)
g': ev_guarded' f (_observe (f i x))
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (_observe (f i x)) g' as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end (evg_unroll_guarded' f (_observe (f i x)) g'))
  (RetF y)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
t: itree E (X +ᵢ Y) i
Heqi0: TauF t = _observe (f i x)
g': ev_guarded' f (_observe (f i x))
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (_observe (f i x)) g' as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end (evg_unroll_guarded' f (_observe (f i x)) g'))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< t))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
Heqi0: VisF q k = _observe (f i x)
g': ev_guarded' f (_observe (f i x))
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (_observe (f i x)) g' as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end (evg_unroll_guarded' f (_observe (f i x)) g'))
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
    all: revert g'; rewrite <- Heqi0; intros g'.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
y: Y i
Heqi0: RetF (inr y) = _observe (f i x)
g': ev_guarded' f (RetF (inr y))
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (RetF (inr y)) g' as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end (evg_unroll_guarded' f (RetF (inr y)) g'))
  (RetF y)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
t: itree E (X +ᵢ Y) i
Heqi0: TauF t = _observe (f i x)
g': ev_guarded' f (TauF t)
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (TauF t) g' as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end (evg_unroll_guarded' f (TauF t) g'))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< t))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
Heqi0: VisF q k = _observe (f i x)
g': ev_guarded' f (VisF q k)
it_eqF E RY (it_eq RY) i
  (match
     evg_unroll' f (VisF q k) g' as t
     return (guarded' t -> itree' E Y i)
   with
   | RetF r0 =>
       match
         r0 as r1
         return (guarded' (RetF r1) -> itree' E Y i)
       with
       | inl x => ex_falso ∘ elim_guarded
       | inr r =>
           fun _ : guarded' (RetF (inr r)) => RetF r
       end
   | TauF t =>
       fun _ : guarded' (TauF t) =>
       TauF
         (iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) i t)
   | VisF q k =>
       fun _ : guarded' (VisF q k) =>
       VisF q
         (fun r : e_rsp q =>
          iter_guarded_aux 
            (eqn_evg_unroll f EG)
            (eqn_evg_unroll_guarded f EG) 
            (e_nxt r) (k r))
   end (evg_unroll_guarded' f (VisF q k) g'))
  (VisF q
     (fun r : e_rsp q =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
    all: dependent elimination g'; econstructor; auto; intros.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
t: itree E (X +ᵢ Y) i
Heqi0: TauF t = _observe (f i x)
g: guarded' (TauF t)
it_eq RY
  (iter_guarded_aux (eqn_evg_unroll f EG)
     (eqn_evg_unroll_guarded f EG) i t)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< t)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
q: e_qry i
k: forall r : e_rsp q, itree E (X +ᵢ Y) (e_nxt r)
Heqi0: VisF q k = _observe (f i x)
g: guarded' (VisF q k)
r: e_rsp q
it_eq RY
  (iter_guarded_aux (eqn_evg_unroll f EG)
     (eqn_evg_unroll_guarded f EG) 
     (e_nxt r) (k r))
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
    all: apply iter_guarded_aux_unfold.
  Qed.

Uniqueness still holds.

  Lemma iter_evg_uniq {X Y RY} {_ : Equivalenceᵢ RY}
    (f : eqn Y X X) (g : X ⇒ᵢ itree E Y)
    (EG : eqn_ev_guarded f)
    (EQ : forall i x,
        it_eq RY
          (g i x)
          (bind (f i x) (fun _ r => match r with
                                 | inl x => g _ x
                                 | inr y => Ret' y end)))
    : forall i x, it_eq RY (g i x) (iter_ev_guarded f EG i x).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' y
    end))
forall (i : I) (x : X i),
it_eq RY (g i x) (iter_ev_guarded f EG i x)
  Proof.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' y
    end))
forall (i : I) (x : X i),
it_eq RY (g i x) (iter_ev_guarded f EG i x)
    unfold it_eq; coinduction R CIH; intros i x.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
it_eq_bt E RY R i (g i x) (iter_ev_guarded f EG i x)
    rewrite iter_evg_unfold, (EQ i x).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
it_eq_bt E RY R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
    remember (EG i x) as Ha; clear HeqHa; unfold ev_guarded in Ha.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
Ha: ev_guarded' f (_observe (f i x))
it_eq_bt E RY R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
    remember (f i x) as t; clear Heqt.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
Ha: ev_guarded' f (_observe t)
it_eq_bt E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
    remember (_observe t) as ot.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
ot: itree' E (X +ᵢ Y) i
Heqot: ot = _observe t
Ha: ev_guarded' f ot
it_eq_bt E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
    revert t Heqot; induction Ha; intros t' Heqot.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
t: itree' E (X +ᵢ Y) i
g0: guarded' t
t': itree E (X +ᵢ Y) i
Heqot: t = _observe t'
it_eq_bt E RY R i
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x, x0: X i
Ha: ev_guarded' f (_observe (f i x0))
IHHa: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_eq_bt E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
t': itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe t'
it_eq_bt E RY R i
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
    -I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
t: itree' E (X +ᵢ Y) i
g0: guarded' t
t': itree E (X +ᵢ Y) i
Heqot: t = _observe t'
it_eq_bt E RY R i
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end)) dependent elimination g0; cbn; rewrite <- Heqot; econstructor; auto; [ | intro r ].I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
t0, t': itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t'
it_eq_t E RY R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end) =<< t0)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< t0)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
t': itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe t'
r: e_rsp e
it_eq_t E RY R (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
      all: eapply (tt_t (it_eq_map E RY)).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
t0, t': itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t'
(it_eq_t E RY ° it_eq_t E RY) R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end) =<< t0)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< t0)
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
t': itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe t'
r: e_rsp e
(it_eq_t E RY ° it_eq_t E RY) R 
  (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
      all: refine (it_eq_up2bind_t _ _ _ _ _ _ _); econstructor; auto.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
t0, t': itree E (X +ᵢ Y) i
Heqot: TauF t0 = _observe t'
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_eq_t E RY R i
  match x1 with
  | inl x => g i x
  | inr y => Ret' y
  end
  match x2 with
  | inl x => iter_ev_guarded f EG i x
  | inr y => Ret' y
  end
I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
t': itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe t'
r: e_rsp e
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_eq_t E RY R i
  match x1 with
  | inl x => g i x
  | inr y => Ret' y
  end
  match x2 with
  | inl x => iter_ev_guarded f EG i x
  | inr y => Ret' y
  end
      all: intros ? ? x2 ->; destruct x2; auto.
    -I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x, x0: X i
Ha: ev_guarded' f (_observe (f i x0))
IHHa: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_eq_bt E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
t': itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe t'
it_eq_bt E RY R i
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t' >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end)) cbn; rewrite <- Heqot.I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x, x0: X i
Ha: ev_guarded' f (_observe (f i x0))
IHHa: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_eq_bt E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
t': itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe t'
it_eqF E RY (it_eq_t E RY R) i 
  (_observe (g i x0))
  (_observe (iter_ev_guarded f EG i x0))
      change (it_eqF E RY ?R i (_observe ?a) (_observe ?b)) with (it_eq_map E RY R i a b).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x, x0: X i
Ha: ev_guarded' f (_observe (f i x0))
IHHa: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_eq_bt E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
t': itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe t'
it_eq_map E RY (it_eq_t E RY R) i 
  (g i x0) (iter_ev_guarded f EG i x0)
      rewrite iter_evg_unfold, (EQ i x0).I: Type
E: event I I
X, Y: psh I
RY: forall x : I, relation (Y x)
H: Equivalenceᵢ RY
f: eqn Y X X
g: X ⇒ᵢ itree E Y
EG: eqn_ev_guarded f
EQ: forall (i : I) (x : X i),
it_eq RY (g i x)
  (f i x >>=
   (fun (i0 : I) (r : (X +ᵢ Y) i0) =>
    match r with
    | inl x0 => g i0 x0
    | inr y => Ret' 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_ev_guarded f EG i x)
i: I
x, x0: X i
Ha: ev_guarded' f (_observe (f i x0))
IHHa: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_eq_bt E RY R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
t': itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe t'
it_eq_map E RY (it_eq_t E RY R) i
  (f i x0 >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => g i x
    | inr y => Ret' y
    end))
  (f i x0 >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
      apply IHHa; auto.
  Qed.

And w.r.t. weak bisimilarity, we still perform the same computation.

  Lemma iter_evg_iter {X Y}
    (f : eqn Y X X) (EG : eqn_ev_guarded f) {i x}
    : iter_ev_guarded f EG i x ≈ iter f i x .I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
iter_ev_guarded f EG i x ≈ iter f i x
  Proof.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
i: I
x: X i
iter_ev_guarded f EG i x ≈ iter f i x
    revert i x; unfold it_wbisim; coinduction R CIH; intros i x.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i (iter_ev_guarded f EG i x)
  (iter f i x)
    eapply (@fbt_bt _ _ (it_wbisim_map E (eqᵢ Y)) _ it_wbisim_up2eq).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
(eq_clo_map ° it_wbisim_bt E (eqᵢ Y)) R i
  (iter_ev_guarded f EG i x) (iter f i x)
    econstructor.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
iter_ev_guarded f EG i x ≊ ?a
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
?b ≊ iter f i x
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i ?a ?b
    apply iter_evg_unfold.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
?b ≊ iter f i x
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end)) ?b
    symmetry; apply iter_unfold.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
it_wbisim_bt E (eqᵢ Y) R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' 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
    |}))
    remember (EG _ x) as g; clear Heqg.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
g: ev_guarded f (f i x)
it_wbisim_bt E (eqᵢ Y) R i
  (f i x >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' 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
    |}))
    remember (f i x) as t; clear Heqt.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
g: ev_guarded f t
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
    unfold ev_guarded in g.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
g: ev_guarded' f (_observe t)
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
    remember (_observe t) as ot.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree E (X +ᵢ Y) i
ot: itree' E (X +ᵢ Y) i
Heqot: ot = _observe t
g: ev_guarded' f ot
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
    revert t Heqot; induction g; intros u Heqot.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree' E (X +ᵢ Y) i
g: guarded' t
u: itree E (X +ᵢ Y) i
Heqot: t = _observe u
it_wbisim_bt E (eqᵢ Y) R i
  (u >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (u >>=
   (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
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisim_bt E (eqᵢ Y) R i
  (u >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (u >>=
   (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
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t: itree' E (X +ᵢ Y) i
g: guarded' t
u: itree E (X +ᵢ Y) i
Heqot: t = _observe u
it_wbisim_bt E (eqᵢ Y) R i
  (u >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (u >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |})) destruct g; cbn ; rewrite <- Heqot; cbn.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
y: Y i
u: itree E (X +ᵢ Y) i
Heqot: RetF (inr y) = _observe u
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (RetF y) (RetF y)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
t, u: itree E (X +ᵢ Y) i
Heqot: TauF t = _observe u
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< t))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< t))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
u: itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe u
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r0 with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< k r))
      econstructor; auto.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t, u: itree E (X +ᵢ Y) i
Heqot: TauF t = _observe u
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       match r with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< t))
  (TauF
     ((fun (i : I) (r : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< t))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
u: itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe u
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       match r0 with
       | inl x => iter_ev_guarded f EG i x
       | inr y => Ret' y
       end) =<< k r))
  (VisF e
     (fun r : e_rsp e =>
      (fun (i : I) (r0 : (X +ᵢ Y) i) =>
       {|
         _observe :=
           match r0 with
           | inl x => TauF (iter f i x)
           | inr y => RetF y
           end
       |}) =<< k r))
      all: econstructor; auto; econstructor; intros.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t, u: itree E (X +ᵢ Y) i
Heqot: TauF t = _observe u
it_wbisim_t E (eqᵢ Y) R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< t)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< t)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
u: itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe u
r: e_rsp e
it_wbisim_t E (eqᵢ Y) R 
  (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< k r)
      all: eapply (tt_t (it_wbisim_map E (eqᵢ Y))).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t, u: itree E (X +ᵢ Y) i
Heqot: TauF t = _observe u
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R i
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< t)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< t)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
u: itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe u
r: e_rsp e
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R
  (e_nxt r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end) =<< k r)
  ((fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}) =<< k r)
      all: refine (it_wbisim_up2bind_t _ _ _ _ _ _ _); econstructor; auto.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t, u: itree E (X +ᵢ Y) i
Heqot: TauF t = _observe u
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_wbisim_t E (eqᵢ Y) R i
  match x1 with
  | inl x => iter_ev_guarded f EG i x
  | inr y => Ret' 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
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
u: itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe u
r: e_rsp e
forall (i : I) (x1 x2 : (X +ᵢ Y) i),
eqᵢ (X +ᵢ Y) i x1 x2 ->
it_wbisim_t E (eqᵢ Y) R i
  match x1 with
  | inl x => iter_ev_guarded f EG i x
  | inr y => Ret' y
  end
  {|
    _observe :=
      match x2 with
      | inl x => TauF (iter f i x)
      | inr y => RetF y
      end
  |}
      all: intros ? ? x2 ->; destruct x2; auto.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t, u: itree E (X +ᵢ Y) i
Heqot: TauF t = _observe u
i0: I
x0: X i0
it_wbisim_t E (eqᵢ Y) R i0
  (iter_ev_guarded f EG i0 x0) (Tau' (iter f i0 x0))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
u: itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe u
r: e_rsp e
i0: I
x0: X i0
it_wbisim_t E (eqᵢ Y) R i0
  (iter_ev_guarded f EG i0 x0) 
  (Tau' (iter f i0 x0))
      all: eapply (tt_t (it_wbisim_map E (eqᵢ Y))).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x: X i
t, u: itree E (X +ᵢ Y) i
Heqot: TauF t = _observe u
i0: I
x0: X i0
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R i0
  (iter_ev_guarded f EG i0 x0) (Tau' (iter f i0 x0))
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x: X i
e: e_qry i
k: forall r : e_rsp e, itree E (X +ᵢ Y) (e_nxt r)
u: itree E (X +ᵢ Y) i
Heqot: VisF e k = _observe u
r: e_rsp e
i0: I
x0: X i0
(it_wbisim_t E (eqᵢ Y) ° it_wbisim_t E (eqᵢ Y)) R i0
  (iter_ev_guarded f EG i0 x0) 
  (Tau' (iter f i0 x0))
      all: cbn; apply it_wbisim_up2eat; econstructor; [ exact EatRefl | exact (EatStep EatRefl) | apply CIH ].
    -I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisim_bt E (eqᵢ Y) R i
  (u >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (u >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |})) cbn; rewrite <- Heqot.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisimF E (eqᵢ Y) (it_wbisim_t E (eqᵢ Y) R) i
  (_observe (iter_ev_guarded f EG i x0))
  (TauF (iter f i x0))
      change (it_wbisimF E (eqᵢ Y) _ _ (_observe ?a) (TauF ?b)) with
        (it_wbisim_bt E (eqᵢ Y) R _ a (Tau' b)).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisim_bt E (eqᵢ Y) R i (iter_ev_guarded f EG i x0)
  (Tau' (iter f i x0))
      eapply (@fbt_bt _ _ (it_wbisim_map E _)).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
?f <= it_wbisim_t E (eqᵢ Y)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
(?f ° it_wbisim_bt E (eqᵢ Y)) R i
  (iter_ev_guarded f EG i x0) 
  (Tau' (iter f i x0))
      refine (it_wbisim_up2eat).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
(eat_clo_map ° it_wbisim_bt E (eqᵢ Y)) R i
  (iter_ev_guarded f EG i x0) (Tau' (iter f i x0))
      econstructor; [ exact EatRefl | exact (EatStep EatRefl) | ].I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisim_bt E (eqᵢ Y) R i (iter_ev_guarded f EG i x0)
  (iter f i x0)
      eapply (@fbt_bt _ _ (it_wbisim_map E _)).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
?f <= it_wbisim_t E (eqᵢ Y)
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
(?f ° it_wbisim_bt E (eqᵢ Y)) R i
  (iter_ev_guarded f EG i x0) 
  (iter f i x0)
      apply (it_wbisim_up2eq).I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
(eq_clo_map ° it_wbisim_bt E (eqᵢ Y)) R i
  (iter_ev_guarded f EG i x0) (iter f i x0)
      econstructor.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
iter_ev_guarded f EG i x0 ≊ ?a
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
?b ≊ iter f i x0
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisim_bt E (eqᵢ Y) R i ?a ?b
      apply iter_evg_unfold.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
?b ≊ iter f i x0
I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i
  (iter_ev_guarded f EG i x) 
  (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (t >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisim_bt E (eqᵢ Y) R i
  (f i x0 >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end)) ?b
      symmetry; apply iter_unfold.I: Type
E: event I I
X, Y: psh I
f: eqn Y X X
EG: eqn_ev_guarded f
R: relᵢ (itree E Y) (itree E Y)
CIH: forall (i : I) (x : X i),
it_wbisim_t E (eqᵢ Y) R i (iter_ev_guarded f EG i x) (iter f i x)
i: I
x, x0: X i
g: ev_guarded' f (_observe (f i x0))
IHg: forall t : itree E (X +ᵢ Y) i,
_observe (f i x0) = _observe t ->
it_wbisim_bt E (eqᵢ Y) R i
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
match r with
| inl x => iter_ev_guarded f EG i x
| inr y => Ret' y
end))
(t >>=
(fun (i : I) (r : (X +ᵢ Y) i) =>
{|
_observe :=
match r with
| inl x => TauF (iter f i x)
| inr y => RetF y
end
|}))
u: itree E (X +ᵢ Y) i
Heqot: RetF (inl x0) = _observe u
it_wbisim_bt E (eqᵢ Y) R i
  (f i x0 >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    match r with
    | inl x => iter_ev_guarded f EG i x
    | inr y => Ret' y
    end))
  (f i x0 >>=
   (fun (i : I) (r : (X +ᵢ Y) i) =>
    {|
      _observe :=
        match r with
        | inl x => TauF (iter f i x)
        | inr y => RetF y
        end
    |}))
      now apply IHg.
  Qed.
End eventually_guarded.