proposition: Lemma EnsembleOfList_In (ls : list W) : forall x, Ensembles.In _ (EnsembleOfList ls) x <-> List.In x ls.
proof: Proof. induction ls; repeat match goal with | _ => split | _ => progress split_iff | [ H : Ensembles.In _ (Ensembles.Add _ _ _) _ |- _ ] => apply Constructive_sets.Add_inv in H | [ H : Ensembles.In _ (Empty_set _) _ |- _ ] => apply Constructive_sets.Noone_in_empty in H | _ => progress destruct_head or | _ => progress destruct_head_hnf Empty_set | _ => intro | _ => progress subst | _ => progress simpl in * | _ => solve [ eauto ] | _ => solve [ right; eauto ] | _ => left; reflexivity | _ => progress unfold EnsembleOfList in * | [ H : context[if ?E then _ else _] |- _ ] => revert H; case_eq E; intros | [ |- context[if ?E then _ else _] ] => case_eq E; intros | [ H : _ |- _ ] => progress rewrite NoFunctionJustFiniteSetOfFunction in H end. handle_calls_then' ltac:(fun H => specialize (H _ (AbsR_EnsembleOfList_FiniteSetOfList _))); pre_t. 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