proposition: Lemma allfv_poly_type_subst_poly_type {P σ t} : allfv_poly_type P (subst_poly_type σ t) <-> (allfv_poly_type (σ >> 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. case; first done. move=> x. rewrite allfv_poly_type_ren_poly_type. by apply: ext_allfv_poly_type. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun