[Consulta general Coq]: Modificar hipótesis

[Consulta general Coq]: Modificar hipótesis

de Lia Malvarez Busquets -
Número de respuestas: 2

Buenas tardes! Hace un tiempo tengo la siguiente duda.

Dadas estas hipótesis:

Hay forma de reescribir (he usado la táctica rewrite para reescribir en goals pero no en hipótesis) por ejemplo la hipótesis H3 con "12 = ( x +++ (x0 +++ 12))".
Dado que esa igualdad (11 = (x0 +++ 12)) está en H4, se me ocurre qué podría hacerse.

Yo en estos casos estoy usando cut (12 = ( x +++ (x0 +++ 12))) y luego pruebo esto usando H4. Pero quisiera saber si directamente pueden reescribirse las hipótesis.

Gracias!

En respuesta a Lia Malvarez Busquets

Re: [Consulta general Coq]: Modificar hipótesis

de Carlos Luna -

Hola.

Vos querés reescribir H4 en H3, verdad?

Fijate: 

rewrite H4 in H3.

Es eso?

Saludos Carlos