proposition: Lemma many_poly_abs_eqE' {n1 n2 s t} : many_poly_abs n1 s = many_poly_abs n2 t -> match s, t with | poly_abs _, _ | _, poly_abs _ => True | _, _ => n1 = n2 /\ s = t end.
proof: Proof. elim: n1 n2. - case. + move=> /= ->. by case: t. + by move=> ? /= ->. - move=> n IH. case. + move=> /= <-. clear. by case: s. + move=> ? [/IH]. clear. case: s; case t; move=> /=; by firstorder lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun