proposition: Lemma L_list_cumulative {X} L : cumulative (@L_list X L).
proof: Proof. intros ?; cbn; eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List