proposition: Lemma erase_ren_term_id {ξ P} : erase (ren_term ξ id P) = erase P.
proof: Proof. elim: P ξ. - done. - by move=> ? + ? + ? /= => -> ->. - move=> ? ? IH ? /=. under extRen_term => [? | ?] do [| rewrite /upRen_term_term up_ren_id]. by rewrite IH. - by move=> ? + ? ? /= => ->. - by move=> ? + ? /= => ->. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts) ssreflect ssrbool ssrfun