proposition: Lemma big_imps A B phi : (A ++ B) ⊢ phi <-> B ⊢ (impl A phi).
proof: Proof. induction A as [|psi A IH] in B,phi|-*; cbn; try tauto. split; intros Hprv. - apply II. apply IH. eapply Weak. 1: apply Hprv. intros x [->|[HA|HB]%in_app_iff]; apply in_app_iff. + right; now left. + now left. + right; now right. - eapply Weak. 1: apply (IH (psi::B)). + eapply IE. 1: eapply Weak; [apply Hprv|firstorder]. apply Ctx; now left. + intros x [HA|[->|HB]]%in_app_iff. * right. apply in_app_iff. now left. * now left. * right. apply in_app_iff. now right. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts