[CTL] Coinduction lemma

[elefthei]

The Coinduction library allows for parametrized coinduction proofs on the shallow definition of ag
but we have no way to do the same kind of proof in the deep definition, for example

We need to unfold entailsF only to do the parametrized coinduction underneath. This exposes the low-level details to the user of the deep embedding. We shouldn't do that and related #29 entailsF should be opaque.
One attempt at defining AG_coind' requires explicitly providing the coinductive relation, which is extremely tedious and cancels all the benefits of parametrized coinduction.

What would it take to do parametrized coinduction proofs without unfolding entailsF and without defining the relation R manually?