proposition: Lemma DNE_Fr {ff} : forall phi Gamma, Gamma ⊢M (dn Q (Fr phi) → @Fr ff phi).
proof: Proof. refine (@size_ind _ size _ _). intros phi sRec. destruct phi; intros Gamma; unfold dn. - apply II. eapply IE; cbn. { apply Ctx; auto. now left. } apply II, Ctx; auto. now left. - apply double_dn. - destruct b0; cbn. + apply II, II. eapply IE. apply sRec; cbn. 1: lia. apply II. eapply IE with (phi:= _ → _). { apply Ctx; auto. try_lr. } apply II. eapply IE with (phi:= Fr phi2). { apply Ctx; auto. try_lr. } eapply IE with (phi:= Fr phi1); apply Ctx; auto. all: try_lr. - destruct q. + cbn. apply II. apply IE with (phi:= ∀ dn Q (Fr phi)). { apply II. constructor. cbn; fold Q. eapply IE. apply sRec; auto. rewrite <-form_up_var0_invar. apply AllE, Ctx; auto. try_lr. } constructor. cbn; fold Q. rewrite <- form_up_var0_invar. apply AllE. cbn; fold Q. now apply imps, dn_forall. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)