proposition: Lemma IndexedElement_TupleToListW_inj : forall {N} (e1 e2: FiatWElement N), IndexedElement_TupleToListW e1 = IndexedElement_TupleToListW e2 -> e1 = e2.
proof: Proof. unfold IndexedElement_TupleToListW; destruct e1, e2; simpl; intros * H; inversion H; subst; clear H; f_equal. apply TupleToListW_inj; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics