subst (lift B i (S k)) j A = (lift B i k).
#A; #B; nelim B; nnormalize; /2/;
##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
subst (lift B i (S k)) j A = (lift B i k).
#A; #B; nelim B; nnormalize; /2/;
##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;