apply (.= (extS_com ??????));
apply (.= (†(respects_converges ?????)));
apply (.= (respects_converges ?????));
apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
apply refl1;
apply (.= (extS_com ??????));
apply (.= (†(respects_converges ?????)));
apply (.= (respects_converges ?????));
apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
apply refl1;
apply (.= (extS_com ??????));
apply (.= (†(respects_all_covered ???)));
apply (.= respects_all_covered ???);
apply refl1]
| intros;
apply (.= (extS_com ??????));
apply (.= (†(respects_all_covered ???)));
apply (.= respects_all_covered ???);
apply refl1]
| intros;