proposition: Lemma prv_T_comp T phi psi xi : T ⋄ phi ⊢T xi -> T ⋄ psi ⊢T phi -> T ⋄ psi ⊢T xi.
proof: Proof. Proof using HF HP. intros (A & HA1 & HA2) % prv_T_impl (B & HB1 & HB2) % prv_T_impl. use_theory (psi :: A ++ B). - now intros psi1 [->|[H1|H2]%in_app_iff]; [now right | |]; left; [apply HA1 | apply HB1]. - eapply IE. 1: eapply Weak. 1: apply HA2. 2: eapply IE. 2-3: eapply Weak. 2: eapply HB2. 3: apply (@Ctx _ _ _ _ (psi::nil)); now left. + intros a Ha; right; apply in_app_iff; now left. + intros b Hb; right; apply in_app_iff; now right. + intros x [->|[]]; now left. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts