proposition: Lemma many_poly_abs_poly_arr_eq_subst_poly_typeE {σ n x t}: many_poly_abs n (poly_arr (poly_var (n+x)) (poly_var (n+x))) = subst_poly_type σ t -> (exists m y, t = many_poly_abs m (poly_var (m+y))) \/ (exists m y1 y2, t = many_poly_abs m (poly_arr (poly_var (m+y1)) (poly_var (m+y2)))).
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=> <-. right. by exists n, x, x. + move=> ?. left. by exists n', (y - n'). - move=> s'' t'' _. rewrite subst_poly_type_many_poly_abs /=. move=> /many_poly_abs_eqE' [<-] []. case: s''; [ | done | done]. case: t''; [ | done | done]. move=> y1 y2 /=. have [?|->] : y1 < n \/ y1 = n + (y1 - n) by lia. + move=> _. rewrite iter_up_poly_type_poly_type_lt; first done. move=> []. by lia. + have [?|->] : y2 < n \/ y2 = n + (y2 - n) by lia. * move=> + _. rewrite iter_up_poly_type_poly_type_lt; first done. move=> []. by lia. * move=> _ _. right. by exists n, (y2-n), (y1-n). - by move=> /=. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun