fact: Fixpoint all_vec {X:Type} {n:nat} {struct n}: (Vector.t X n -> Prop) -> Prop := match n with 0 => fun A => A (@Vector.nil _) | S n => fun A => forall x, all_vec (fun xs => A (x:::xs)) end.
imports: Undecidability(TM.Util.TM_facts)