proposition: Lemma exist_dn phi Gamma: Gamma ⊢M ((∃ (dn Q phi)) → dn Q (∃ phi)).
proof: Proof. apply II, II. eapply ExE. { apply Ctx; auto. right. now left. } cbn; fold Q. apply IE with (phi:= phi → Q). { apply Ctx; auto. now left. } apply II. eapply IE with (phi:= ∃ _). { apply Ctx; auto. do 2 right. now left. } eapply ExI. rewrite form_up_var0_invar. apply Ctx; auto. now left. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FullSyntax) Undecidability.FOL.Arithmetics(Robinson NatModel)