Hola.
Para formalizar el lemma SKK=I va a ser necesario poner los tipos adecuados. Esto es, determinar los tipos ?i en:
Lemma e52 : forall ... : Set, (opS ?1 ?2 ?3 (opK ?4 ?5) (opK ?6 ?7)) = opI ?8.
Una ayuda con los dos primeros: ?1 puede ser un tipo A y ?2: una flecha (función) como: B -> A.
Saludos, Carlos