Buenas,
¿Solo se pueden utilizar las tácticas vistas en el teórico y sobre las mismas hipótesis?
Ej. En mi caso, utilice apply H con H:= A /\ B para demostrar B (un poco mas corto que usar elim) y utilice apply H con H := A <-> B (evito hacer el unfold).
Saludos.
Hola Bruno.
Has avanzado mucho, felicitaciones!
Pueden usar tácticas adicionales, mientras entiendan bien que están haciendo, no hoy problema. De a poco en el curso esto se irá viendo y se permitirá usar algunas cosas de Coq incluso adicionales a las que veamos en el curso.
Saludos Carlos