fix proof broken by slight change to cakeml repo
probable fix to constrain_assignment_def, and new thm

about constrain_interpretation being a subinterpretation