Formalization progress of controlled subtyping in Coq

Tasks

• Improve automation, renaming
  • reasoning with in fv_ctt_m
    • seen in “csub_mu_modular_aux”