proposition: Lemma allfv_pure_term_ren_pure_term {p ξ M} : allfv_pure_term p (ren_pure_term ξ M) <-> allfv_pure_term (ξ >> p) M.
proof: Proof. elim: M ξ p. - done. - move=> ? IH1 ? IH2 > /=. by rewrite IH1 IH2. - move=> ? IH > /=. rewrite IH. constructor; apply: allfv_pure_term_impl; by case. 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