Commit 2026-05-16 04:19 415af1a6

feat(fun_prop): allow fun_prop to call discharger on ModelWithCorners (#39226) Currently, a discharger in fun_prop is allowed to be run only on Prop-valued hypothesis. This PR allows to execute dischargers also on ModelWithCorners. This will enable fun_prop to support ContMDiff properly: lemmas like ContMDiff.comp require inferring the model with corners on the intermediate space. This PR is thus required to properly support manifolds in fun_prop; a future PR will implement this. In the future, we might want to allow the discharger to execute on other Type-valued hypothesis. In this case, we could create an environment extension to register such types. However, right now we could not think of any other use cases --- therefore, we hard-coded ModelWithCorners.