proposition: Lemma PA2_enumerable : enumerable PA2.
proof: Proof. exists (fun n => List.nth n (List.map Some PA2_L) None). intros phi. split. - intros H. repeat destruct H as [<-|H]. now exists 0. now exists 1. now exists 2. now exists 3. now exists 4. now exists 5. now exists 6. now exists 7. now exists 8. easy. - intros [n H]. assert (forall x y : form, Some x = Some y -> x = y) as Some_inj by congruence. do 9 try destruct n as [|n]; try apply Some_inj in H as <-. 1-9: easy. now destruct n. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec