Problem when running one of the examples

[Calugar25]

When i try to run the "forall x. P(x) implies (Q(x) implies P(x))" example i get multiple errors , do you know why that could be ?

[stepchowfun]

I barely remember how this code works, so I might not be able to help. It would be good if you could say what errors you're seeing.