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