proposition: Lemma MND_CND A (phi : form falsity_off) : A ⊢M phi -> map cast A ⊢C cast phi.
proof: Proof. revert A phi. remember falsity_off as b. intros. induction H; cbn in *; subst; try congruence. - eapply II; eauto. - eapply IE; try now apply IHprv1. now apply IHprv2. - eapply AllI. rewrite map_map. rewrite map_map in IHprv. erewrite map_ext; try now apply IHprv. intros psi. cbn. now rewrite subst_cast. - setoid_rewrite subst_cast. eapply AllE; eauto. - eapply Ctx, in_map_iff; eauto. - apply Pc. Qed.
imports: Undecidability.PCP(PCP Util.PCP_facts) Undecidability.FOL(Deduction.FragmentNDFacts Semantics.Tarski.FragmentFacts Semantics.Tarski.FragmentSoundness Syntax.Core Syntax.Facts) Undecidability.FOL(FOL) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ReducibilityFacts MoreReducibilityFacts) Undecidability.FOL.Reductions.PCPb_to_FOL Undecidability.PCP.Reductions.PCPb_iff_dPCPb List Undecidability(Shared.ListAutomation)