proposition: Lemma double_dn Gamma F phi : Gamma ⊢M dn F (dn F phi) → dn F phi.
proof: Proof. apply II, II. eapply IE with (phi:= _ → _). { apply Ctx; firstorder. } apply II. apply IE with (phi:= phi → F). all: apply Ctx; cbv;eauto. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FullSyntax) Undecidability.FOL.Arithmetics(Robinson NatModel)