proposition: Lemma tupleAgree_equivalence' : forall {h} tup1 tup2 attrlist, @tupleAgree_computational h tup1 tup2 attrlist <-> @tupleAgree_computational' h tup1 tup2 attrlist.
proof: Proof. induction attrlist; simpl; intros. - intuition eauto. - destruct attrlist; simpl. + intuition. + simpl in *; intuition eauto. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Common.ilist2 Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Constraints.DuplicateFree Fiat.Computation.Core Fiat.Computation.Refinements.General Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Automation.Common