proposition: Lemma Lift_Ensemble : forall n r idx (el: FiatWTuple n), Ensembles.In _ r {| IndexedEnsembles.elementIndex := idx; IndexedEnsembles.indexedElement := el |} <-> Ensembles.In _ (IndexedEnsemble_TupleToListW r) {| TuplesF.elementIndex := idx; TuplesF.indexedElement := TupleToListW el |}.
proof: Proof. split; intros. - econstructor; intuition eauto. unfold RelatedIndexedTupleAndListW; split; simpl; eauto. - destruct H; unfold RelatedIndexedTupleAndListW in *; intuition. simpl in *; subst. destruct x; simpl in *; subst. unfold TupleToListW in H2. apply ilist2ToListW_inj in H2; subst; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW CertifiedExtraction.Extraction.QueryStructures.CallRules.CallRules CertifiedExtraction.Extraction.QueryStructures.Wrappers Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Bedrock.Platform.Facade.CompileUnit2 CertifiedExtraction.ADT2CompileUnit CertifiedExtraction.Extraction.Extraction CertifiedExtraction.Extraction.QueryStructures.Decompose Bedrock.Memory Bedrock.Platform.Facade.DFModule Bedrock.Platform.Facade.CompileUnit2