inline the lex ordering axiom for precedes when building the type environment for recursive call
inline the lex ordering axiom for precedes when building the type environment for recursive call

FStarLang/FStar,FStarLang/FStar,FStarLang/FStar