- 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 (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (b↓c))));
+ unfold FunClass_1_OF_Type_OF_setoid21;
+ alias symbol "trans" = "trans1".
+ apply (.= († (respects_converges : ?)));
+ apply (respects_converges ?? t (t1\sub\f⎻ b) (t1\sub\f⎻ c));
+ | change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (oa_one (form o3)))));
+ unfold FunClass_1_OF_Type_OF_setoid21;
+ apply (.= (†(respects_all_covered :?)));
+ apply rule (respects_all_covered ?? t);]