- 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;