proposition: Lemma LL_f n : f n el LL (S n).
proof: Proof. induction (lt_acc n) as [n _ IH]. decide (f n el LL (S n)); try assumption. exfalso. assert (H : ~ f n el LL n). { intros H. apply n0. apply (cum_ge' LL_cum H). auto. } apply gen_le_f in H as [n'[H1 H2] ]. specialize (H2 n eq_refl). destruct (Nat.lt_total n' n) as [H3|[->|H3] ]. - apply (gen_spec (A:=LL n)). rewrite <- H1. now apply (cum_ge' LL_cum (IH n' H3)). - apply n0. rewrite H1. apply in_app_iff; fold LL. right. left. reflexivity. - lia. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia