clean up the subinterpretation stuff

i.e. finish extension of proof of extends_consistent
fix error in statement of infinity ax

hadn't specialised the type variables to Ind