proposition: Lemma vec_Forall2_append {X Y : Type} {P : X -> Y -> Prop} {n m : nat} {v : Vector.t X n} {w : Vector.t X m} {v' w'} : Vector.Forall2 P v v' -> Vector.Forall2 P w w' -> Vector.Forall2 P (Vector.append v w) (Vector.append v' w').
proof: Proof. elim. { done. } move=> > ? _ /[apply] ?. by constructor. Qed.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun