proposition: Lemma F_lt n m : n < m -> F n el LL m.
proof: Proof. intros H. apply (cum_ge' (n:=S n)). - apply LL_cum. - apply F_el. - lia. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia