theorem lsubf_sor: ∀K,L,g1,f1. ⦃K, g1⦄ ⫃𝐅* ⦃L, f1⦄ →
∀g2,f2. ⦃K, g2⦄ ⫃𝐅* ⦃L, f2⦄ →
- â\88\80g. g1 â\8b\93 g2 â\89¡ g â\86\92 â\88\80f. f1 â\8b\93 f2 â\89¡ f → ⦃K, g⦄ ⫃𝐅* ⦃L, f⦄.
+ â\88\80g. g1 â\8b\93 g2 â\89\98 g â\86\92 â\88\80f. f1 â\8b\93 f2 â\89\98 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