apply Free.eq.bisim
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ corec (bind.automaton f) (Sum.inr x) = x
case a
C : _root_.Container
R S : Type u₁
f : R → Free C S
x : Free C S
⊢ eq (corec (bind.automaton f) (Sum.inr x)) x