proposition: Lemma enumerator__T_term : enumerator__T term_enumerator__T term.
proof: Proof. intros t. unfold term_enumerator__T. enough (exists n, forall m, n <= m -> term_enum_rec (S m) n = t) as [n Hn]. { exists n. f_equal. now apply Hn. } induction t as [n|s [n1 IHs] t [n2 IHt]|s [n IH]]. - exists (Cantor.to_nat (0, n)). cbn. now rewrite Cantor.cancel_of_to. - exists (Cantor.to_nat (S (S n1), n2)). cbn. assert (H' := Cantor.to_nat_non_decreasing (S (S n1)) n2). intros [|m] ?. { lia. } rewrite !Cantor.cancel_of_to, IHs, IHt; [easy | lia | lia]. - exists (Cantor.to_nat (1, n)). cbn. assert (H' := Cantor.to_nat_non_decreasing 1 n). intros [|m] ?. { lia. } rewrite !Cantor.cancel_of_to, IH; [easy | lia ]. Qed.
imports: Undecidability.Synthetic.EnumerabilityFacts Undecidability.L.L Lia