proposition: Lemma typing_ren_term {ξ Gamma Delta P t} : (forall n s, nth_error Gamma n = Some s -> nth_error Delta (ξ n) = Some s) -> typing Gamma P t -> typing Delta (ren_term id ξ P) t.
proof: Proof. move=> H /[dup] [/typing_allfv_term_in_environment HP] /typing_ren_allfv_term. apply. by apply: allfv_term_impl HP => ? [?] /[dup] [/H] -> ->. 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