exists node
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
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ 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)
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
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (i : B C node), R (k₁ i) (k₂_1 i)