case mk node k₂ =>
  rw [h₁] at h₀
  simp only [construct, destruct_corec, Map] at h₀
  simp only [construct.automaton, Map] at h₀
  exists node
  exists λ (x:B C i node) => construct <| destruct <| k₂ x
  exists k₂
  constructor
  . exact h₀
  . constructor
    . rfl
    . intro i
      rfl
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
h₀ : destruct x = destruct (construct (destruct 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₂ }
⊢ ∃ 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)
no goals