proposition: Lemma allfv_pure_term_erase {p P}: allfv_pure_term p (erase P) -> allfv_term p P.
proof: Proof. elim: P p; [ done | | | done | done ]. - by move=> ? IH1 ? IH2 > /= [/IH1 ? /IH2 ?]. - by move=> > IH > /= /IH. 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