- change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
- change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
- with (c1 \sub \f ∘ c \sub \f);
- change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
- with (c1 \sub \f ∘ c \sub \f);
- apply (.= (extS_com ??????));
- apply (.= (†(respects_converges ?????)));
- apply (.= (respects_converges ?????));
- apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
- apply refl1;
- | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
- apply (.= (extS_com ??????));
- apply (.= (†(respects_all_covered ???)));
- apply (.= respects_all_covered ???);
- apply refl1]
+ change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2))));
+ alias symbol "trans" = "trans1".
+ apply (.= († (Orespects_converges : ?)));
+ apply (Orespects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2));
+ | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (Oform o3)))));
+ apply (.= (†(Orespects_all_covered :?)));
+ apply rule (Orespects_all_covered ?? c);]