prepare lemma
minor
minor
modify driver
put lemma in comment
put mappings in driver file
simplify proof
checkin in between
use old names