proposition: Lemma all_vec_correct {X:Type} {n:nat} (P : Vector.t X n -> Prop): all_vec P -> forall xs, P xs.
proof: Proof. revert P. induction n;cbn;intros. - now apply Vector.case0. - intros. apply Vector.caseS'. intro. now eapply IHn. Qed.
imports: Undecidability(TM.Util.TM_facts)