# Re: [isabelle] coinduct_upto for coinductive predicates

Hallo,

`thanks for the explanation. I think I now managed to define the closure
``that I need and prove the corresponding coinduct_upto rule.
`

`I noticed that during the proof of this rule, I essentially needed to
``prove that all the friendly functions in the closure preserve the
``inductive predicate, i.e. in terms of the example theory from earlier, I
``needed to prove some generalised version of "P s ==> P (g s)".
`

`I then thought that once I have proven the coinduct_upto rule, I should
``be able to easily derive the fact "P s ==> P (g s)" from that, but I
``cannot see how. If I want to prove "P s ==> P (g s)", do I really have
``to do all the proof work again?
`
Cheers,
Manuel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*