-fact lexs_dropable_dx_aux: â\88\80RN,RP,b,f,L2,K2. â¬\87*[b, f] L2 â\89¡ K2 → 𝐔⦃f⦄ →
- â\88\80f2,L1. L1 ⪤*[RN, RP, f2] L2 â\86\92 â\88\80f1. f ~â\8a\9a f1 â\89¡ f2 →
- â\88\83â\88\83K1. â¬\87*[b, f] L1 â\89¡ K1 & K1 ⪤*[RN, RP, f1] K2.
+fact lexs_dropable_dx_aux: â\88\80RN,RP,b,f,L2,K2. â¬\87*[b, f] L2 â\89\98 K2 → 𝐔⦃f⦄ →
+ â\88\80f2,L1. L1 ⪤*[RN, RP, f2] L2 â\86\92 â\88\80f1. f ~â\8a\9a f1 â\89\98 f2 →
+ â\88\83â\88\83K1. â¬\87*[b, f] L1 â\89\98 K1 & K1 ⪤*[RN, RP, f1] K2.