assume as b:Bool -> {v:Int | b == True}
assume = 0
assert as {b:Bool | b == True} -> Int
assert = 0
bool as Bool
bool = 0
succ :: b:Int ~> ({u:Int | b <= u} -> Int) -> {u:Int | b <= u} -> Int
succ = \f x -> f (x + 1)
app3 :: a:Int ~> ({u:Int | a <= u} -> Int) -> b:Int ~> (c:Int ~> ({u:Int | a <= u} -> Int) -> Int) -> Int
app3 = \f g -> if bool then app3 (succ f) g else g f
app :: x:Int -> a:Int ~> ({u:Int | x <= u} -> Int) -> Int
app = \x f -> f x
check :: x:Int -> {u:Int | x <= u} -> Int
check = \x y -> if x <= y then 1 else assert False
main :: Int -> Int
main = \i -> app3 (check i) (app i)