Started working on the inferencer side conditions

Proved `t_wfs st.subst ==> infer_e_side menv cenv env e st` using 2
cheats, which arise from the bad side conditions on (at least)
apply_subst_list_side_def:

∀v4. apply_subst_list_side v4 ⇔ ∀v3. t_wfs v3.subst