Hola,
Estoy teniendo un error en Coq con esta parte de la planilla:
Theorem e231: H1 /\ H2 -> ...
Coq me tira el error:
The term "H1" has type "forall x : U, R x x" while it is expected to have type "Prop".
Probe copiar directamente el contenido de la hipótesis H1 en el Theorem y me funciona,
Sera algún problema con la planilla ?
Saludos y gracias!