proposition: Lemma term_to_nat_pos t : term_to_nat t = S (Nat.pred (term_to_nat t)).
proof: Proof. by case: t. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun