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 construct ∘ destruct ∘ k₂
  exists k₂
  constructor
  . exact h₀
  . constructor
    . rfl
    . intro i
      rfl
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
node : C.A
k₂ : B C node → M C
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 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
no goals