- [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
- | intros;
- 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 (c1 ∘ c);
+ | intros;
+ change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2))));
+ alias symbol "trans" = "trans1".
+ apply (.= († (respects_converges : ?)));
+ apply (.= (respects_converges : ?));