pcofix is powerful but you can often get cleaner proofs by working directly in the
νF carrier and using the universal property of finality. The coinduction
principle you want is: two elements of the final coalgebra are equal iff they are
bisimilar. Write your bisimulation relation, show it's a coalgebra morphism, done.
∀ x y. R x y → R (out x) (out y) ⊢ x = y