This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
letrec [ | |
fun succ_known_101<302>(x_438) := | |
case x_438 of { | |
| xI => | |
let p_439 := proj_0 144 x_438 in | |
let y_440 := app succ_known_101<302>(p_439) in | |
let y_441 := xO(y_440) in | |
halt y_441 | |
| xO => |