proposition: Lemma tupleAgree_unfold : forall {heading} (tup1 tup2: @RawTuple heading) attr more, tupleAgree tup1 tup2 (attr :: more) <-> (GetAttributeRaw tup1 attr = GetAttributeRaw tup2 attr) /\ tupleAgree tup1 tup2 more.
proof: Proof. unfold tupleAgree; simpl; split; intros; intuition; subst; intuition. Qed.
imports: Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Schema