proposition: Theorem Fr_cl_to_min {ff} Gamma phi : Gamma ⊢C phi -> (@Fr_ ff Gamma) ⊢M Fr phi.
proof: Proof. induction 1; unfold Fr_ in *; cbn in *. - now constructor. - econstructor; eassumption. - constructor. now rewrite subst_Fr_. - eapply AllE with (t:=t) in IHprv. now rewrite subst_Fr in IHprv. - specialize (DNE_Fr phi (map Fr A)) as H'. eapply IE; [eassumption|]. cbn; apply II. eapply Weak; eauto. apply incl_tl, incl_refl. - now apply Ctx, in_map. - apply Peirce_Fr. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)