proposition: Lemma prv_embed { p : peirce } A phi : A ⊢ phi -> (map embed A) ⊢ embed phi.
proof: Proof. intros H. pattern p, A, phi. revert p A phi H. apply prv_ind_full; cbn; intros; subst; auto. 6-9: eauto. - eapply IE. 1: apply H0. easy. - apply AllI. apply (Weak H0). rewrite !map_map. intros psi' [psi [<- HP]] % in_map_iff. apply in_map_iff. eexists. split; try apply HP. rewrite embed_subst. apply subst_ext. reflexivity. - apply (AllE (embed_t t)) in H0. rewrite embed_subst. erewrite subst_ext; try apply H0. now intros [|n]. - apply (ExI (embed_t t)). rewrite embed_subst in H0. erewrite subst_ext; try apply H0. now intros [|n]. - eapply ExE; try apply H0. rewrite embed_subst in H2. erewrite subst_ext; try apply (Weak H2); try now intros [|n]. rewrite !map_map. intros theta' [<-|[theta [<- HP]] % in_map_iff]; auto. right. apply in_map_iff. eexists. split; try apply HP. rewrite embed_subst. apply subst_ext. reflexivity. - apply Ctx. now apply in_map. Qed.
imports: Undecidability.FOL(Semantics.Tarski.FullFacts Syntax.Facts Deduction.FullNDFacts) Undecidability.FOL.Sets(ZF minZF) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_minZF PCPb_to_ZFD) Undecidability(Shared.ListAutomation)