(* Main properties **********************************************************)
-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ā¦.
#K elim K -K
[ #L #g1 #f1 #H1 #g2 #f2 #H2 #g #Hg #f #Hf
elim (lsubf_inv_atom1 ā¦ H1) -H1 #H1 #H destruct