Add more detail in descend lemma

One more FIXME to go
Fix the last FIXME from restricted.tex