Prove last admitted lemmas
Fix and prove lift_subst_semicom
Rename lift_subst_semicom into lift_distr_subst

Because that's what it is.