proposition: Lemma impl_prv A B phi : (rev B ++ A) ⊢ phi -> A ⊢ (B ==> phi).
proof: Proof. revert A; induction B; intros A; cbn; simpl_list; intros. - firstorder. - eapply II. now eapply IHB. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts