Split basis proofs into separate directory

The proofs about the basis program depend on CF, but the construction of the program itself probably doesn't. Splitting the proofs off into a separate subdirectory could make it possible to, e.g., make process topdecs do type inference including the basis program as @hrutvik mentioned wanting to do at some point. (It's not obvious this is a good idea yet, so discussion after poking around is welcome.)