proposition: Lemma ilist2ToListW_inj : forall n el el', ilist2ToListW (N := n) el = ilist2ToListW el' -> el = el'.
proof: Proof. induction n; simpl; eauto. - destruct el; destruct el'; reflexivity. - destruct el; destruct el'; simpl; intros. unfold ilist2.ilist2_tl, ilist2.ilist2_hd in *; simpl in *. injections; f_equal. eapply IHn; eassumption. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics