proposition: Lemma L_nat_correct n m : m <= n -> m el L_nat n.
proof: Proof. induction n. - intros H. left. lia. - intros H. cbn. assert (m = S n \/ m <= n) as [] by lia; firstorder. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec List