Added "using" to the beginning of original newman proof again, because
it was lost during last update; renamed second version of newman to
newman' (this allows for a comparison of the primitive proof objects,
for example).
(*Dummy theory to document dependencies *)
coinductive = "ind_syntax" + "intr_elim"