fact: Definition IsPrefix_dec : forall (p s : list X), {IsPrefix p s} + {~ IsPrefix p s} := @Prefix_dec _ A_eq_dec (fun a => eq_refl a).
imports: Coq.Lists.SetoidList Fiat.QueryStructure.Specification.Representation.QueryStructureNotations