proposition: Lemma encode_sym_inj s1 s2 : encode_sym s1 = encode_sym s2 -> s1 = s2.
proof: Proof. unfold encode_sym. intros H. eapply Fin.to_nat_inj. revert H. generalize (proj1_sig (Fin.to_nat s1)) (proj1_sig (Fin.to_nat s2)). intros n0. clear s1 s2. revert n. induction n0 as [|n0 IH]. - now intros [|n] [|n1]. - intros [|n] [|n1]; [easy| |easy|]. + cbn. now intros [= ->%(IH 0)]. + cbn. now intros [= ->%IH]. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators