First datastructures for the proof engine

	new file:   ocaml/proof.ml
	new file:   ocaml/term.ml
	new file:   ocaml/type.ml