fix(library/coinductive_predicates): fix existential types

[cipher1024]

coinductive_predicates would work badly when given an existential type such as:

coinductive rel : ℕ → ℕ → Prop
| trans (x y z : ℕ) :
  rel x y → rel y z → rel x z

Now it works and produces the following corecursion principle:

rel.corec_on :
  ∀ (C : ℕ → ℕ → Prop) {a a_1 : ℕ},
    C a a_1 → (∀ (a a_1 : ℕ), C a a_1 → (∃ (y : ℕ), C a y ∧ C y a_1)) → rel a a_1

[johoelzl]

Uh why do the other test cases fail now?

[cipher1024]

The problem was that my use of unify seems only valid for existential types. So I'm making a case distinction now.

[Kha]

Coinductive predicates are being moved to mathlib.

[cipher1024]

Thanks!