. intro 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 construct ∘ destruct ∘ k₂
    exists k₂
    constructor
    . exact h₀
    . constructor
      . rfl
      . intro i
        rfl
case h₀
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)

case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x