proposition: Lemma UniuqeListOfList_cons_UniqueFilterOfList a f ls : UniqueListOfList (a::UniqueFilterOfList ls f) = if negb (andb (snd ((CallMethod (projT1 FiniteSetImpl) sIn) (FiniteSetOfList ls) a) ) (f a)) then a::UniqueFilterOfList ls f else UniqueFilterOfList ls f.
proof: Proof. unfold UniqueListOfList, FunctionOfList; simpl. rewrite NoFunctionJustFiniteSetOfFunction. repeat handle_calls''. rewrite EnsembleOfList_In in *. rewrite In_UniqueFilterOfList in *. rewrite !NoFiniteSetJustListOfList. rewrite UniqueListOfUniqueFilterOfList. repeat match goal with | _ => progress simpl in * | _ => progress destruct_head bool | _ => progress destruct_head and | _ => progress destruct_head False | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) | _ => progress split_iff | [ H : ?x = true |- context[?x] ] => rewrite H | [ H : ?x = false |- context[?x] ] => rewrite H | [ H : ?T -> false = true |- _ ] => assert (T -> False) by (let t := fresh in intro t; specialize (H t); inversion H); clear H | _ => reflexivity | [ H : false = true -> _ |- _ ] => clear H | [ H : _ -> ?x = ?x |- _ ] => clear H | [ H : _ /\ ?T -> ?U, H' : ?T |- _ ] => specialize (fun k => H (conj k H')) | [ H : ?T -> ?U, H' : ?T |- _ ] => specialize (H H') | [ H : _ = true -> False |- _ ] => apply Bool.not_true_is_false in H 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