proposition: Lemma last_poly_var_t_cs : last_poly_var t_cs = Some tt.
proof: Proof. rewrite /t_cs. move: (_ ++ _) => ss. move: (tt) => x. elim: (δ) x. - move=> x. by elim: ss. - move=> n + x /=. have ->: S (n + x) = n + S x by lia. by move=> ->. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun