rename lemmas
collect generic lemmas into the front
clean up
prove prop3c
use "private" construct
generalize some lemmas