proposition: Lemma vec_inv2 {X} (v : Vector.t X 2) : v = [Vector.hd v; Vector.hd (Vector.tl v)].
proof: Proof. apply (Vector.caseS' v). intros x w. apply (Vector.caseS' w). intros ?. now apply Vector.case0. 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 Undecidability.Synthetic.Definitions