proposition: Lemma many_poly_absI t : exists n s, t = many_poly_abs n s /\ not (is_poly_abs s).
proof: Proof. elim: t. - move=> >. exists 0. eexists. by constructor. - move=> >. exists 0. eexists. by constructor. - move=> t [n] [s] [-> ?]. exists (1+n). by eexists. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun