The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

[To: 
coq-club AT pauillac.inria.fr]

On Tue, 1 Jul 2003, Russell O'Connor wrote:

> [To: 
> coq-club AT pauillac.inria.fr]
>
> Can someone explain to me the conditions neccesary on the Goal in order
> for Dependent Rewrite to work?

To answer my own question, I beleive the requirement is the type of the
Goal has to be of the form

([x:A][y:(B x)](P x y)) a b  for some P

when trying to use Dependent Rewrite on
(existS A B a b)=(existS A B a' b')

Maybe someone can confirm if I'm right or not.

- -- 
Russell O'Connor                <http://math.berkeley.edu/~roconnor/>
                Work to ensure that Iraq is run by Iraqis.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.1 (SunOS)

iQCVAwUBPwIvyU0+aO5oRkNZAQK0UgQApfadB+a0QIZPGlXzPYdRfLfpfiZtDf7J
Lj5FxZsaPcUHEpYVg6nQmvkxnQ6jCDqUrn3RzH9QPgdJmgWdhQd9OHUKe0Ho/oXJ
uT5dVVtO5UigFL/0kmS6Vvt5XqoU/hTQlw5r9SlzXmiBtXdpdJ/YL91Sp7h/yI0O
aRRFcYfgGMg=
=Bgd2
-----END PGP SIGNATURE-----