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. - split; intros. + eapply II. now eapply IHB. + now apply imps, IHB in H. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia