simp only [construct.automaton, Map] at h₀
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    match construct.automaton i { fst := node, snd := k₂ } with
    | { fst := x, snd := k } => { fst := x, snd := fun y => corec construct.automaton (k y) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)