proposition: Lemma TupleToListW_indexed_inj {N}: forall (t1 t2: FiatWElement N), TupleToListW_indexed t1 = TupleToListW_indexed t2 -> t1 = t2.
proof: Proof. destruct t1, t2; unfold TupleToListW_indexed; simpl. intro eq; inversion eq; subst; clear eq. f_equal; intuition. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics