proposition: Lemma ren_pure_term_id' {ξ M} : (forall x, ξ x = x) -> ren_pure_term ξ M = M.
proof: Proof. move=> ?. rewrite -[RHS]ren_pure_term_id. by apply: extRen_pure_term. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts Undecidability.SystemF.Util.poly_type_facts ssreflect ssrbool ssrfun