Consultas de Práctico

Hola, haciendo el práctico 1 me surgieron varias dudas. Aclaro por las dudas que me miré las primeras 3 clases de la edición del año pasado que están en openfing como referencia principal (y naturalmente la curiosidad llevó a googlear un poco también).

1. A la hora de hacer intro/intros, el nombre que se le asigna a las variables si uno no lo explicita se puede asumir que va a ser el mismo independientemente de quien lo corra y su entorno? Es decir, si yo en mi prueba hago referencia a un H3 que nombró automáticamente coq en mi máquina, en la de cualquier otra persona también va a ser ese mismo H3 y no va a dar problemas por ese lado?
2. Basado en que Carlos en una clase del año pasado dijo que podíamos subir pedacitos de código aunque fueran parte de los ejercicios entregables y confiando en que como el ejercicio es trivial y por ende no le voy a cambiar la vida a nadie exponiendo esta solución, me permito mostrar estas líneas: 
   
   Lemma conmOr: forall A B : Prop, A\/B -> B\/A.
   Proof. 
     intros.
     elim H.
     intro.
     right.
     assumption.
     intro.
     left.
     assumption.
   Qed.
   (* Ej 6.2 *)
   Theorem e622: A\/B <-> B\/A.
   Proof. 
     cut (forall A B : Prop, A\/B -> B\/A).
     2:exact conmOr.
     intro.
     split.
     specialize (H A B).
     assumption.
     specialize (H B A).
     assumption.
    Qed.
   
   Sobre esto tengo varias preguntas: Es legal usar lemas de esa forma para los entregables aunque todavía no lo hayamos visto en el curso? Entiendo que con lo visto se puede hacer sin problema (y termina quedando más o menos igual de largo) pero cuando lo empecé a hacer me pedía a gritos algún reciclaje de código de este tipo. Hay alguna forma más limpia o eficiente de hacerlo? Ejemplo, para probar el iff no hace falta hacer unfold not; hay alguna otra cosa por esas líneas que se pueda hacer para acortarlo? Cuando quiero cambiar de objetivo principal la forma en la que lo hice arriba sólo lo hace por esa línea. Hay alguna forma de hacerlo para todas las líneas que siguen en caso de necesitar aplicar más de una táctica para probarlo?
3. En el ej 10 que pide usar tauto, las pruebas serían sólo usar tauto una vez y listo? Qué sentido tiene hacer esto con más de un teorema de los anteriores? En el caso de los que no son intuicionistas entiendo que falla, pero en los que sí va a ser todo lo mismo, o me equivoco?
4. Para el 11 leí en un mensaje del foro de una edición anterior que se podía usar classic, pero yo no lo necesité. Me estoy perdiendo de algo?
5. En el 12 también encontré un mensaje que decía que se podía usar classic y en este tanto yo intentando hacerlo intuicionista durante 2 horas como tauto fallamos, así que asumo que efectivamente es necesario pero lo dejo como pregunta por las dudas para confirmar.
6. Varias veces me pasó, en particular jugando con tauto que dentro de la demostración de un teorema coq toma las hipótesis de teoremas anteriores. Cómo se puede hacer para aislarlos y no tener este problema? Fue particularmente problemático cuando por tener las hipótesis (inconsistentes) del club escocés tauto podía probar el 12. Un primer intento por tapar este problema fue comentar todo el ejercicio 11 mientras hacía el 12, pero cuando lo terminé y descomenté resulta que todas las hipótesis provenientes de intros que coq nombró automáticamente hacen que las que genero en la prueba del 12 se llamen distinto y la prueba se rompa... Parece un problema que le debe haber pasado a alguien antes y que uno querría asumir que tiene una solución simple.

Mis agradecimientos de antemano a la pobre alma que le toque leer este garrón y se tome la molestia de contestar.

Saludos,

Gabriel