-lemma deg_rel_not_le: ∀K,L,i. (S i) ≰ |L| →
- ║Rel i║_[L @ K] = ║Rel (i-|L|)║_[K].
-#K #L elim L -L [ normalize // ]
-#l #L #IHL #i elim i -i [1: -IHL #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
-normalize #i #_ #Hie @IHL /2/
+lemma deg_rel_not_le: ∀L,K,i. (S i) ≰ |K| →
+ ║Rel i║_[K @ L] = ║Rel (i-|K|)║_[L].
+#L #K elim K -K [ normalize // ]
+#k #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
+normalize #i #_ #Hie @IHK /2/