proposition: Lemma rm_dn Gamma F alpha beta : (alpha :: Gamma) ⊢M beta -> (dn F alpha :: Gamma) ⊢I dn F beta.
proof: Proof. intros H. apply II. eapply IE with (phi:= _ → _). { apply Ctx; firstorder. } apply II. eapply IE with (phi:= beta). { apply Ctx; cbv;eauto. } eapply Weak. 1:eassumption. apply cons_incl_proper, incl_tl, incl_tl, incl_refl. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)