proposition: Lemma nat_term_cancel {t} : nat_to_term (term_to_nat t) = t.
proof: Proof. rewrite /nat_to_term. move Hk: (k in nat_to_term' (1 + k) _) => k. have : term_to_nat t <= k by lia. elim: t k {Hk}. - done. - move=> x k /=. by rewrite Cantor.cancel_of_to. - move=> nt IHt nu IHu k /=. rewrite Cantor.cancel_of_to => ?. have ? := Cantor.to_nat_non_decreasing (S (term_to_nat nt)) (S (term_to_nat nu)). have -> : k = S (k - 1) by lia. rewrite IHt; first by lia. by rewrite IHu; first by lia. - move=> nt IH k /=. rewrite Cantor.cancel_of_to => ?. have ? := Cantor.to_nat_non_decreasing (S (term_to_nat nt)) 0. have -> : k = S (k - 1) by lia. by rewrite IH; first by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun