proposition: Lemma many_poly_abs_eqE'' {n1 t1 n2 t2} : many_poly_abs n1 t1 = many_poly_abs n2 t2 -> not (is_poly_abs t2) -> exists n3, t1 = many_poly_abs n3 t2 /\ n2 = n1 + n3.
proof: Proof. elim: n2 n1. - move=> [|?]. + move=> /= <- _. by exists 0. + by move=> /= <- /=. - move=> n1 IH [|n2]. + move=> /= -> _. by exists (1+n1). + move=> [/IH H] /H [n3] [-> ->]. by exists n3. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun