proposition: Lemma fset_finite : forall E, exists L, E = from_list L.
proof: Proof. Proof using. intros [U [L' H]]. exists (filter (fun x => isTrue (is_in x U)) L'). apply fset_extens_eq. intros x. rewrite from_list_spec. unfold mem at 1. simpl. extens. iff M. { specializes H M. induction L'. { inverts H. } { rewrite filter_cons. inverts H. { rewrite (prop_eq_True M). rewrite~ isTrue_True. case_if; tryfalse*. auto. } { case_if*. } } } { clear H. induction L'. { rewrite filter_nil in M. inverts M. } { rewrite filter_cons in M. cases_if~. { inverts~ M. } } } Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)