proposition: Lemma tupleAgree_empty : forall {heading} (tup1 tup2: @RawTuple heading), tupleAgree tup1 tup2 nil <-> True.
proof: Proof. unfold tupleAgree; intuition. Qed.
imports: Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Schema