1 translations
2 "case l of up`x => t1" == "lift`(¤x.t1)`l"
2 "case l of up`x => t1" == "fup`(¤x.t1)`l"
3