Incomplete handling of cumulativity in native

[SkySkimmer]

(* dummy let to avoid the syntactic equality fast path *)
Definition nativecast@{u v|u < v} (x:let _ := tt in Type@{u}) := (x <<: Type@{v}).
(* fails *)

This is because native puts the context into the terms to be converted as lambdas (let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in ...), but then converting the bodies of lambdas ignores the conv_pb and always uses CONV.

BTW we build those lambdas before we check if native is enabled, so the VM fallback gives the same error even though directly calling the VM works fine.