simp only [corec, destruct]
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ destruct (corec f x₀) = Map (corec f) (f x₀)
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ {
      fst :=
        node
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) },
      snd :=
        children
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) } } =
    Map
      (fun x₀ =>
        { approx := Approx.corec f x₀,
          agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) })
      (f x₀)