// output = output.replace(/lambda/g, "\u03BB");
// output = output.replace(/exists/g, "\u2203");
// output = output.replace(/forall/g, "\u2200");
// output = output.replace(/lambda/g, "\u03BB");
// output = output.replace(/exists/g, "\u2203");
// output = output.replace(/forall/g, "\u2200");