-lemma liftsb_split_trans: â\88\80f,I1,I2. â¬\86*[f] I1 â\89¡ I2 →
- â\88\80f1,f2. f2 â\8a\9a f1 â\89¡ f →
- â\88\83â\88\83I. â¬\86*[f1] I1 â\89¡ I & â¬\86*[f2] I â\89¡ I2.
+lemma liftsb_split_trans: â\88\80f,I1,I2. â¬\86*[f] I1 â\89\98 I2 →
+ â\88\80f1,f2. f2 â\8a\9a f1 â\89\98 f →
+ â\88\83â\88\83I. â¬\86*[f1] I1 â\89\98 I & â¬\86*[f2] I â\89\98 I2.