∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (enc enc_1 : Γ → List.Vector Bool n) (e_enc : enc = enc_1)
  [inst : Inhabited Γ] (enc0 : enc default = List.Vector.replicate n false) (a a_1 : Turing.TM1.Cfg Γ Λ σ),
  a = a_1 → Turing.TM1to1.trCfg enc enc0 a = Turing.TM1to1.trCfg enc_1 ⋯ a_1