o added proofs by disjunction
o fixed the calculation of free variables in parsing progress properties
o added a proper test
o fixed for the proofs by disjunction