proposition: Lemma typing_ren_term' {ξ Gamma Delta P t} : (forall n, nth_error Gamma n = nth_error Delta (ξ n)) -> typing Gamma P t -> typing Delta (ren_term id ξ P) t.
proof: Proof. move=> H /typing_ren_term. apply => ? ?. by rewrite 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