proposition: Lemma to_list_in' X n (v : Vector.t X n) x : x el Vector.to_list v -> Vector.In x v.
proof: Proof. induction v; cbn. - inversion 1. - inversion 1; subst; try now left. right. apply IHv, H0. 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