proposition: Lemma refine_Iterate_Equiv_QueryResultComp_body_Where_False m {ResultT : Type} (heading : RawHeading) (headings : Fin.t m -> RawHeading) (Ensembles : forall (idx : Fin.t m), @IndexedEnsemble (@RawTuple (headings idx))) (inj_Tuple : forall (idx : Fin.t m), @RawTuple (headings idx) -> @RawTuple heading) (FiniteEnsembles : forall idx, FiniteEnsemble (Ensembles idx)) (body : @RawTuple heading -> Comp (list ResultT)) P : (forall idx tup, In _ (Ensembles idx) tup -> ~ P (inj_Tuple idx (indexedElement tup))) -> refine (Iterate_Equiv_QueryResultComp_body heading headings Ensembles inj_Tuple (fun tup : RawTuple => Where (P tup) (body tup) )) (ret nil).
proof: Proof. induction m; simpl; intros. - reflexivity. - rewrite refine_QueryResultComp_body_Where_False; eauto. simplify with monad laws. apply IHm; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.SumType Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Bedrock.Word Bedrock.Memory