-theorem lsubf_sor: āK,L,g1,f1. ā¦K, g1ā¦ ā«š
* ā¦L, f1ā¦ ā
- āg2,f2. ā¦K, g2ā¦ ā«š
* ā¦L, f2ā¦ ā
- āg. g1 ā g2 ā g ā āf. f1 ā f2 ā f ā ā¦K, gā¦ ā«š
* ā¦L, fā¦.
+theorem lsubf_sor:
+ āK,L,g1,f1. ā¦K,g1ā¦ ā«š
+ ā¦L,f1ā¦ ā
+ āg2,f2. ā¦K,g2ā¦ ā«š
+ ā¦L,f2ā¦ ā
+ āg. g1 ā g2 ā g ā āf. f1 ā f2 ā f ā ā¦K,gā¦ ā«š
+ ā¦L,fā¦.