--- opening "BadConstraint.ma" --- --- scope checking --- scope check error: f /// |i| < |i|: constraints must follow a quantifier