fact: Definition ForeignKey_P heading relSchema attr1 attr2 tupmap (tup : @RawTuple heading) (R : Ensemble (@IndexedRawTuple relSchema)) := exists tup2, R tup2 /\ GetAttributeRaw tup attr1 = tupmap (GetAttributeRaw (indexedRawTuple tup2) attr2).
imports: Coq.Lists.List Coq.Strings.String Fiat.Common Coq.Arith.Arith Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.StringBound Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Schema Fiat.QueryStructure.Specification.Representation.Relation