proposition: Lemma ren_pure_term_id {M} : ren_pure_term id M = M.
proof: Proof. elim: M. - done. - move=> /=. congruence. - move=> /=. rewrite /upRen_pure_term_pure_term. move=> > ?. under extRen_pure_term => ? do rewrite up_ren_id. by congruence. 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