probably going to rethink how I should go about formalizing this; finramsey should be trashed (except the proof outline)