proposition: Lemma map_hd X Y n (f : X -> Y) (v : Vector.t X (S n)) : Vector.hd (Vector.map f v) = f (Vector.hd v).
proof: Proof. now apply (Vector.caseS' v). Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List