Initial commit; implementation of lob's theorem
Update proof to use implication, not equality