bug_15221.out

chain =
fun x y : nat => let/c f := foo x y in
                 let/c b := bar x y in
                 f = b
     : nat -> nat -> Prop

Arguments chain (x y)%nat_scope