proposition: Lemma fset_extens_eq : forall E F, (forall x, x \in E = x \in F) -> E = F.
proof: Proof. Proof using. unfold mem. intros [U FU] [V FV] H. simpls. apply exist_eq_exist. apply in_extens. intros. rewrite* H. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)