lambda-where-fullproofs