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. - apply II. eapply IE. + apply Ctx. firstorder. + apply Weak with (A := map Fr A); [|apply incl_tl, incl_refl]. apply ExI with (t:=t). now rewrite subst_Fr. - eapply IE. apply DNE_Fr. unfold dn in *; cbn. apply II. eapply IE. { eapply Weak; [apply IHprv1|auto]. apply incl_tl,incl_refl. } apply II. eapply IE. { apply Ctx; auto. try_lr. } rewrite <-subst_Fr, <-subst_Fr_ in IHprv2. eapply ExE. { apply Ctx; auto. try_lr. } cbn. eapply Weak; [apply IHprv2|auto]. apply cons_incl_proper, incl_tl, incl_tl, incl_refl. - 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. - now apply CI. - eapply CE1; eauto. - eapply CE2; eauto. - apply II. eapply IE. + apply Ctx. auto. try_lr. + apply DI1. eapply Weak; eauto. apply incl_tl, incl_refl. - apply II. eapply IE. + apply Ctx; auto. try_lr. + apply DI2. eapply Weak; eauto. apply incl_tl, incl_refl. - eapply IE. apply DNE_Fr. apply II. eapply IE. { eapply Weak; [apply IHprv1|auto]. apply incl_tl, incl_refl. } apply II. eapply IE. { apply Ctx; auto. try_lr. } apply imps in IHprv2. apply imps in IHprv3. eapply DE. 1 : apply Ctx; firstorder. 1,2 : apply imps; eapply Weak; [eassumption|auto]; apply incl_tl, incl_tl, incl_refl. - apply Peirce_Fr. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FullSyntax) Undecidability.FOL.Arithmetics(Robinson NatModel)