renamed CaseCheck → Soundness
new theory for nVCG soundness
moved admissible_input back for cleaner theory import graphs
minor documentation adjustments