proposition: Lemma typing_allfv_term_in_environment {Gamma P t} : typing Gamma P t -> allfv_term (fun x => exists s, nth_error Gamma x = Some s) P.
proof: Proof. elim => /=. - move=> > ->. by eexists. - done. - move=> > ?. apply: allfv_term_impl. by case. - done. - move=> > ?. apply: allfv_term_impl => ?. rewrite nth_error_map. case: (nth_error _ _); last by case. move=> *. by eexists. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts term_facts) ssreflect ssrbool ssrfun