- lapply (.= †e); [3: apply rule t \sub \f; |4: apply Hletin; |1,2: skip]
- cut ((t \sub \f ∘ (⊩)) ∘ (⊩)* = ?);
- [
-
- lapply (Hcut U); apply Hletin;
- whd in Hcut;: apply rule (rel BP2);
-
- generalize in match U; clear e;
- change with (t \sub \f ((⊩) ((⊩)* U)) =(⊩) ((⊩)* (t \sub \f U)));
- change in ⊢ (? ? ? % ?) with ((t \sub \f ∘ ((⊩) ∘ (⊩)* )) U);
-
-
+ apply sym1;
+ alias symbol "refl" = "refl1".
+ apply (.= †?); [1: apply (t \sub \f (((◊_BP1∘(⊩)* ) U))); |
+ lapply (†e); [2: apply rule t \sub \f; | skip | apply Hletin]]
+ change in ⊢ (? ? ? % ?) with ((◊_BP2 ∘(⊩)* ) ((t \sub \f ∘ (◊_BP1∘(⊩)* )) U));
+ lapply (comp_assoc2 ????? (⊩)* (⊩) t \sub \f);
+ apply (.= †(Hletin ?)); clear Hletin;
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
+ cut ?;
+ [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e3 ^ -1 ((⊩)* U));] | 2,4: skip]
+ apply (.= †Hcut);
+ change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
+ apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+ apply (.= Hcut ^ -1);
+ change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+ apply (prop11 ?? t \sub \f);
+ apply (e ^ -1);