proposition: Lemma erase_ren_term {ξ σ P} : erase (ren_term σ ξ P) = ren_pure_term ξ (erase P).
proof: Proof. elim: P ξ σ. - done. - by move=> ? + ? + ? ? /= => -> ->. - by move=> ? ? + ? ? /= => ->. - done. - 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