proposition: Lemma derivations_derivable B n s t : (s, t) el derivations B n -> derivable B s t.
proof: Proof. Proof using M_FST VIEQ. induction n in s,t|-*; cbn. - now constructor. - unfold derivation_step. intros [[u v][H1 H2]] % in_flat_map. unfold append_all in H2. apply in_map_iff in H2 as [[a b][H2 H3]]. cbn in H2. assert (s = u++a) as -> by congruence. assert (t = v++b) as -> by congruence. constructor 2; trivial. apply IHn, H3. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.FST Undecidability.FOL.Sets.FST Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)