apply equivF.Free
case a.Free
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)
⊢ equivF Eq
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
      pequiv Eq fun x y => x = corec (bind.automaton f) (Sum.inr y))
    (construct
      (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)))
    (construct (Functor.Free n k))
case a.Free.a
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)
⊢ ∀ (x : Container.B C n),
    ((fun x y => x = corec (bind.automaton f) (Sum.inr y)) ⊔
        pequiv Eq 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)
        x)
      (k x)