proposition: Lemma allfv_poly_type_ren_poly_type {P ξ t} : allfv_poly_type P (ren_poly_type ξ t) <-> (allfv_poly_type (ξ >> P) t).
proof: Proof. elim: t ξ P. - done. - by move=> /= ? + ? + ? ? => -> ->. - move=> ? /= IH ? ?. rewrite IH. apply: ext_allfv_poly_type. rewrite /scons /funcomp. by case. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun