Fix: Witness must be real witness

If the goal is 'some(a,b,...) exp' the prover searches for a term 't'
and a substitution 'sub' such that 'exp' substituted by 'sub' equals
't'. But the term 't' serves as a witness only if it has at least one
subterm for each of the variables 'a,b,...' i.e. if the substitution
is complete.

If the substitution is not complete the witness is not a real witness
for the existentially quantified assertion.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/term.ml
Extracted 'proof_term' to the module 'proof.ml'

	new file:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
	modified:   ocaml/prover.ml