IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
type_inj is intended chiefly for injecting into quotienttypes. For convenience, typing lemmas should be provenfor each application. e.g. ... x:T. [x]{a,b:T//Eab}A general typing lemma for type_inj(x;T) cannotbe proven, because it's antecedent would involve the subtypepredicate which isn't typeable.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x:T. [x]{a,b:T//Eab}A general typing lemma for type_inj(x;T) cannotbe proven, because it's antecedent would involve the subtypepredicate which isn't typeable.