proposition: Lemma tupleAgree_equivalence : forall {h} tup1 tup2 attrlist, @tupleAgree h tup1 tup2 attrlist <-> @tupleAgree_computational h tup1 tup2 attrlist.
proof: Proof. induction attrlist; simpl; intros. apply tupleAgree_empty. rewrite tupleAgree_unfold, IHattrlist. reflexivity. Qed.
imports: Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Schema