Copy a theorem from machine.v to smooth.v Cleanup todo: re-prove the theorem in machine.v from the general statement and proof in smooth.v
Copy a theorem from machine.v to smooth.v
Cleanup todo: re-prove the theorem in machine.v from the general
statement and proof in smooth.v

gstew5/cage,gstew5/cage