proposition: Lemma Double' b A (phi : form b) : A ⊢C phi -> map trans A ⊢I trans phi.
proof: Proof. remember class as s; induction 1; subst. - cbn. eapply II. eauto. - eapply IE; eauto. - cbn. apply AllI. rewrite map_map. rewrite map_map in IHprv. erewrite map_ext; try now apply IHprv. intros psi. cbn. now rewrite trans_subst. - setoid_rewrite trans_subst. eapply AllE; eauto. - specialize (IHprv eq_refl). eapply IE; try apply trans_trans. apply II. apply (Weak IHprv). auto. - eapply Ctx. now eapply in_map. - eapply IE; try apply trans_trans. apply II. eapply IE; try now apply Ctx. cbn. apply II. eapply IE; try now apply Ctx. apply II. eapply IE; try apply trans_trans. apply II. eapply IE. + apply Ctx. right. right. right. now left. + apply II. apply Ctx. auto. 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)