proposition: Lemma ens_red {heading} {BagType TSearchTerm TUpdateTerm} : forall (y_is_bag: Bag BagType (@Tuple heading) TSearchTerm TUpdateTerm) x y, @EnsembleIndexedListEquivalence (@Tuple heading) x (benumerate (Bag := y_is_bag) y) = (ID (fun y => EnsembleIndexedListEquivalence x (benumerate y))) y.
proof: Proof. intros; reflexivity. Qed.
imports: Coq.Strings.String Coq.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.Common.List.ListFacts