proposition: Lemma counters_eta (v : vec nat 5) : v = Vector.hd v ## Vector.hd (Vector.tl v) ## Vector.hd (Vector.tl (Vector.tl v)) ## Vector.hd (Vector.tl (Vector.tl (Vector.tl v))) ## Vector.hd (Vector.tl (Vector.tl (Vector.tl (Vector.tl v)))) ## Vector.nil _.
proof: Proof. do 5 (rewrite [LHS](Vector.eta v); congr Vector.cons; move: (Vector.tl v) => {}v). by apply: vec_0_nil. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun