add theorem and definitions in H spec list; start proof