proposition: Lemma vec_Forall2_forall {X Y : Type} {P : X -> Y -> Prop} {n : nat} {v : Vector.t X n} {w : Vector.t Y n} : (forall i, P (Vector.nth v i) (Vector.nth w i)) <-> Vector.Forall2 P v w.
proof: Proof. split. - elim: v w. + move=> w ?. rewrite (vec_0_nil w). by constructor. + move=> > IH w. rewrite (Vector.eta w) => IH'. constructor. * by apply: (IH' pos0). * apply: IH => i. by apply: (IH' (pos_nxt i)). - elim. { by apply: Fin.case0. } move=> > ? _ IH i. have [->|[j ->]] := pos_S_inv i. + done. + by apply: IH. 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