. intro i x y h₀
  have h₀ := congrArg destruct h₀
  cases h₁:destruct y
  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
case 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),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)

case a
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)
⊢ R i (construct (destruct x)) x
case a
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)
⊢ R i (construct (destruct x)) x