(*** sor_mono *)
corec theorem pr_sor_mono:
- â\88\80f1,f2,x,y. f1 â\8b\93 f2 â\89\98 x â\86\92 f1 â\8b\93 f2 â\89\98 y â\86\92 x â\89¡ y.
+ â\88\80f1,f2,x,y. f1 â\8b\93 f2 â\89\98 x â\86\92 f1 â\8b\93 f2 â\89\98 y â\86\92 x â\89\90 y.
#f1 #f2 #x #y * -f1 -f2 -x
#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
[ cases (pr_sor_inv_push_bi … H … H1 H2)