proposition: Fact GammaS1Sn {n} : GammaS1 (S n) = GammaS1 n ++ [St (poly_num n, poly_num 1, poly_num (1+n))].
proof: Proof. by rewrite (ltac:(lia) : S n = n + 1) /GammaS1 seq_app map_app. 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