proposition: Lemma big_imps_nil A phi : A ⊢ phi <-> [] ⊢ (impl A phi).
proof: Proof. specialize (big_imps A nil phi). rewrite app_nil_r. easy. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts