proposition: Lemma In_UniqueFilterOfList f ls x : List.In x (UniqueFilterOfList ls f) <-> f x = true /\ List.In x ls.
proof: Proof. unfold UniqueFilterOfList, FunctionOfList; simpl. induction ls. { simpl; split; tauto. } { simpl in *; intros. rewrite !NoFunctionJustFiniteSetOfFunction. rewrite !NoFiniteSetJustFunctionOfList. rewrite !NoFiniteSetJustFunctionOfList in IHls. handle_calls''. rewrite EnsembleOfList_In in *. repeat match goal with | [ H : ?T -> ?U, H' : ?T |- _ ] => specialize (H H') | [ |- _ <-> _ ] => split | [ |- _ /\ _ ] => split | _ => intro | _ => progress simpl in * | _ => progress split_iff | _ => progress split_and | _ => progress destruct_head bool | _ => progress destruct_head_hnf or | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) | _ => progress subst | _ => right; assumption | [ H : ?x = true, H' : context[?x] |- _ ] => rewrite H in H' | [ H : ?x = true |- context[?x] ] => rewrite H | [ H : false = true -> _ |- _ ] => clear H | [ H : ?T -> false = true |- _ ] => assert (T -> False) by (let t := fresh in intro t; specialize (H t); inversion H); clear H | [ |- false = true ] => exfalso | [ H : false = true |- _ ] => inversion H | _ => tauto | [ H : context[if ?E then _ else _] |- _ ] => revert H; case_eq E | [ |- context[if ?E then _ else _] ] => case_eq E 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