proposition: Lemma agreeAllAttributes_eq : forall heading tup tup', tupleAgree_computational' tup tup' (allAttributes heading) <-> tup = tup'.
proof: Proof. setoid_rewrite <- tupleAgree_equivalence'. destruct heading. induction AttrList; unfold RawTuple; simpl; intros. - destruct tup; destruct tup'; intuition. - destruct tup; destruct tup'; simpl. intuition. + unfold GetAttributeRaw in H0; simpl in H0; unfold ilist2_hd in H0; simpl in H0; subst. unfold allAttributes in IHAttrList. rewrite (proj1 (IHAttrList prim_snd prim_snd0)); eauto; simpl. revert H1. induction (BuildFinUpTo n); simpl; intuition. + injections; eauto. + injections. generalize (proj2 (IHAttrList prim_snd0 prim_snd0) eq_refl); clear. induction (BuildFinUpTo n); simpl; intuition. 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