proofs: add ROOT for c-refinement and ROOTS for cogent Additionally, reorganise imports so that things actually work