proposition: Lemma trans_trans' b (phi : form b) A sigma tau : (map (subst_form tau) A) ⊢I ((dnQ (trans phi[sigma])) → trans phi[sigma]).
proof: Proof. revert A sigma tau. induction phi; cbn; intros; try destruct P; try destruct b0; try destruct q. - cbn. eapply II. eapply app1. eapply II. eapply Ctx. eauto. - eapply II. eapply II. eapply app2. eapply II. eapply app1. eapply Ctx. eauto. - eapply II. eapply app1. eapply II. eapply Ctx. eauto. - eapply II. eapply II. apply IE with (dnQ (trans phi2[sigma])). specialize (IHphi2 A sigma tau). apply (Weak IHphi2). auto. eapply II. eapply app3. eapply II. eapply app2. eapply app1. eapply Ctx. eauto. - apply II, AllI. apply IE with (dnQ (trans phi[up sigma])). + apply IHphi. + apply II. eapply IE. { apply Ctx. right. left. cbn. reflexivity. } apply II. eapply IE. { apply Ctx. right. left. reflexivity. } replace (trans phi[up sigma]) with (((trans (phi[up sigma]))[up ↑])[($0)..]) at 4. * apply AllE. apply Ctx. now left. * setoid_rewrite trans_subst. cbn. repeat setoid_rewrite subst_comp. apply subst_ext. intros n. unfold funcomp. cbn. apply subst_term_id. now intros []. 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)