Fix admits in lemmas related to `mwiden` and al.
Remove wrongly (assumed) axioms