proper sort constraints for strip_shyps, which implicitly performs type instantiation;
include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer;