rfl
case a.Free.a.h
C : _root_.Container
R S : Type u₁
f : R → Free C S
x✝ x y✝ : Free C S
n : C.A
k : Container.B C n → Free C S
hy : destruct y✝ = Functor.Free n k
h₂ :
  destruct x =
    Functor.Free n
      ((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
y : Container.B C n
⊢ (fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (((corec fun x =>
          match x with
          | Sum.inr x =>
            match destruct x with
            | Functor.Pure r => Functor.Pure r
            | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
          | Sum.inl x =>
            match destruct x with
            | Functor.Pure r =>
              match destruct (f r) with
              | Functor.Pure r => Functor.Pure r
              | Functor.Free node k => Functor.Free node (Sum.inr ∘ k)
            | Functor.Free n k => Functor.Free n (Sum.inl ∘ k)) ∘
        Sum.inr ∘ k)
      y)
    (k y)
no goals