proposition: Lemma UniqueListOfUniqueFilterOfList f ls : UniqueListOfList (UniqueFilterOfList ls f) = UniqueFilterOfList ls f.
proof: Proof. induction ls; unfold UniqueListOfList, UniqueFilterOfList, FunctionOfList in *; simpl in *; trivial. rewrite !NoFiniteSetJustListOfList in IHls |- *. rewrite !NoFiniteSetJustFunctionOfList. rewrite !(pull_if UniqueListOfList). unfold UniqueListOfList, UniqueFilterOfList, FunctionOfList in *; simpl in *; trivial. rewrite !NoFiniteSetJustFilterFunctionOfList in IHls |- *. rewrite !NoFunctionJustFiniteSetOfFunction. rewrite !NoFiniteSetJustFunctionOfList in IHls |- *. rewrite IHls. repeat handle_calls''. rewrite EnsembleOfList_In in *. rewrite In_UniqueFilterOfList in *. repeat match goal with | [ |- appcontext[if ?E then _ else _] ] => case_eq E | _ => intro | _ => progress subst | _ => reflexivity | [ H : ?x = true, H' : context[?x] |- _ ] => rewrite H in H' | _ => progress split_iff | _ => progress split_and | [ H : ?x = ?x /\ _ -> _ |- _ ] => specialize (fun k => H (conj eq_refl k)) | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) | [ H : ?T -> ?U, H' : ?T |- _ ] => specialize (H H') | _ => congruence 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