proposition: Lemma map_TupleToListW_inj {N}: forall (t1 t2: list (@RawTuple (MakeWordHeading N))), map TupleToListW t1 = map TupleToListW t2 -> t1 = t2.
proof: Proof. induction t1; simpl; destruct t2; simpl; intros; try discriminate. - reflexivity. - inversion H; f_equal; eauto with inj_db. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics