proposition: Lemma vector_cast_refl (X : Type) (n1 : nat) (H1 : n1 = n1) (v : Vector.t X n1) : Vector.cast v H1 = v.
proof: Proof. induction v; cbn; f_equal; auto. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Code.Code Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi