Buenas.
Avanzando en la demostración haciendo inducción en n1, para el paso base (n1 = 0) llegue a tener que probar que:
S2 = S1
Donde mis hipotesis son las siguientes:
i : Instr
S1, S2 : Memoria
H : Execute (irepeat 0 i) S1 S2
Crei que haciendo inversion en H la prueba saldria muy facilmente dado la regla xRepeatO de Execute:
rxRepeatO : forall (i: Instr)(S: Memoria), Execute (irepeat 0 i) S S
El problema es que al hacer inversion se me generan 2 pruebas, S2 = S2 (facil con reflexivity) y nuevamente S2 = S1, no me queda claro porque se genera esa segunda prueba.