That proofs B must be a subtype of A since `B: A` is a bound on the exit type argument.

# functional

[raulraja]

That proofs B must be a subtype of A since B: A is a bound on the exit type argument.