âb,f,K1. đâŚf⌠â âŠ*[b,f] L1 â K1 â
ââK2. G ⢠K1 âŤâ K2 & âŠ*[b,f] L2 â K2.
#G #L1 #L2 #H elim H -L1 -L2
âb,f,K1. đâŚf⌠â âŠ*[b,f] L1 â K1 â
ââK2. G ⢠K1 âŤâ K2 & âŠ*[b,f] L2 â K2.
#G #L1 #L2 #H elim H -L1 -L2