proposition: Lemma fresh_in_many_poly_absI {x n t} : fresh_in (n+x) t -> fresh_in x (many_poly_abs n t).
proof: Proof. move=> H. apply /allfv_poly_type_many_poly_absI. apply: allfv_poly_type_impl H => y ?. have [?|?] : y < n \/ n <= y by lia. - by rewrite iter_scons_lt. - rewrite iter_scons_ge; by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun