proposition: Lemma enc_string_inj s t : M_enc_string s = M_enc_string t -> s = t.
proof: Proof. Proof using M_FST VIEQ. induction s in t|-*; destruct t as [|b t]; cbn; trivial. - intros H. contradiction (@M_eset (M_sing (M_enc_bool b))). rewrite H. apply M_pair. now left. - intros H. contradiction (@M_eset (M_sing (M_enc_bool a))). rewrite <- H. apply M_pair. now left. - intros [H1 H2] % opair_inj. apply IHs in H2 as ->. apply enc_bool_inj in H1 as ->. reflexivity. 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)