proposition: Lemma TupleToListW_inj {N}: forall (t1 t2: @RawTuple (MakeWordHeading N)), TupleToListW t1 = TupleToListW t2 -> t1 = t2.
proof: Proof. induction N; simpl; destruct t1, t2; simpl; intros. - reflexivity. - inversion H; f_equal; 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