- Equality check on propositions after lookup of theorem now takes type variable
renamings into account
- Unconstrain theorem after lookup
- Improved error messages for application cases
Bool = FOL +
types bool 0
arities bool :: term
consts tt,ff :: "bool"
end