proposition: Lemma many_poly_abs_poly_var_eq_subst_poly_typeE {σ n x t}: many_poly_abs n (poly_var (n+x)) = subst_poly_type σ t -> exists i m y, n = i + m /\ t = many_poly_abs m (poly_var (m+y)).
proof: Proof. have [n' [t' [-> +]]] := many_poly_absI t. case: t'. - move=> y _. rewrite subst_poly_type_many_poly_abs /=. have [?|->] : y < n' \/ y = n' + (y - n') by lia. + rewrite iter_up_poly_type_poly_type_lt; first done. move=> <-. by exists 0, n, x. + move=> /esym /many_poly_abs_eqE'' /(_ ltac:(done)). move=> [n''] [? ->]. exists n'', n', (y - n'). constructor; [by lia | done]. - move=> ? ? _. rewrite subst_poly_type_many_poly_abs /=. by move=> /many_poly_abs_eqE' []. - by move=> /=. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun