BadConstraint1.err

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