proposition: Lemma Check_List_Prop_dec' {A} : forall (cond : A -> bool) (P : Ensemble A) (l : list A), (forall a, cond a = true <-> P a) -> (Check_List_Prop cond l = false <-> (exists a', List.In a' l /\ ~ P a')).
proof: Proof. split; induction l; simpl; intros; intuition; subst. generalize (H a); find_if_inside; intuition; eauto. destruct_ex; intuition; intuition; eauto. eexists; intuition. destruct_ex; intuition. generalize (H a); find_if_inside; intuition; eauto. destruct_ex; subst; intuition; eauto. subst; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.ADTRefinement.BuildADTRefinements Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.QueryStructureRefinements Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements