File let-with-axioms.fmsl, line 1, char 12: Type of axiom expression must be boolean File let-with-axioms.fmsl, line 2, char 13: Type of axiom expression must be boolean File let-with-axioms.fmsl, line 3, char 12: Let expr only allowed in an expr sequence. File let-with-axioms.fmsl, line 4, char 21: y is not defined in this scope. File let-with-axioms.fmsl, line 5, char 20: y is not defined in this scope. File let-with-axioms.fmsl, line 8, char 5: Type of axiom expression must be boolean