-lemma fsle_pair_bi: â\88\80K1,K2. |K1| = |K2| â\86\92 â\88\80V1,V2. â\9dªK1,V1â\9d« â\8a\86 â\9dªK2,V2â\9d« →
- â\88\80I1,I2. â\9dªK1.â\93\91[I1]V1,#Oâ\9d« â\8a\86 â\9dªK2.â\93\91[I2]V2,#Oâ\9d«.
+lemma fsle_pair_bi: â\88\80K1,K2. |K1| = |K2| â\86\92 â\88\80V1,V2. â\9d¨K1,V1â\9d© â\8a\86 â\9d¨K2,V2â\9d© →
+ â\88\80I1,I2. â\9d¨K1.â\93\91[I1]V1,#Oâ\9d© â\8a\86 â\9d¨K2.â\93\91[I2]V2,#Oâ\9d©.