proposition: Lemma list_filter_pred_In {T} P (ls : list T) v : computes_to (list_filter_pred P ls) v -> forall x, List.In x v -> List.In x ls.
proof: Proof. revert v; induction ls; simpl; intros. { inversion_by computes_to_inv; subst; simpl in *; trivial. } { repeat match goal with | [ H : computes_to (Bind _ _) _ |- _ ] => apply computes_to_inv in H | [ H : computes_to (ret _) _ |- _ ] => apply computes_to_inv in H | _ => progress destruct_head ex | _ => progress destruct_head and | _ => progress inversion_by computes_to_inv | _ => progress subst | _ => progress destruct_head bool | _ => progress destruct_head or | _ => progress split_iff | [ H : true = true -> _ |- _ ] => specialize (H eq_refl) | _ => left; reflexivity | _ => right; solve [ eauto ] end. } Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.RelationPairs Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Computation Fiat.Common Fiat.Common.Ensembles Fiat.Common.Ensembles.Tactics Fiat.ComputationalEnsembles Fiat.FiniteSetADTs.FiniteSetADTMethodLaws Fiat.FiniteSetADTs.FiniteSetADT