Fix proofs.

Lebesgue/Set_theory/Set_system/Topology.v

@@ -74,13 +74,10 @@ Lemma all_is_Basisf : is_Basisf T (skolem T).
 Proof.
 split.
 intros [x Hx]; easy.
-(*
-intros A HA; exists (fun i => incl (proj1_sig i) A).
-apply set_ext_equiv; split; intros x Hx.
-exists (exist _ _ HA); split; easy.
-destruct Hx as [[A' HA'] [Hx1 Hx2]]; apply Hx1, Hx2.
-*)
-Admitted.
+intros A HA; apply set_ext_equiv; split; intros x.
+intros; exists (exist _ _ HA); easy.
+intros [[B HB1] [HB2 HB3]]; auto.
+Qed.
 
 Lemma all_is_Basisp : is_Basisp T T.
 Proof.
@@ -92,42 +89,19 @@ Qed.
 
 Variable fB : Idx -> set U.
 
+(* Useful? *)
 Lemma Basisf_to_Basisp : is_Basisf T fB -> is_Basisp T (unskolem fB).
 Proof.
-intros [HfB1 HfB2]; split.
-intros B [i]; auto.
-(*
-intros A HA; destruct (HfB2 A HA) as [P HP]; rewrite HP.
-rewrite unionf_any_unionp_any_eq.
-apply set_ext_equiv; split; intros x Hx.
-(* *)
-destruct Hx as [B [HB1 HB]]; induction HB1 as [i]; destruct HB as [HB1 HB2].
-exists (fB i); repeat split; try easy.
-intros y Hy; exists (fB i); split; try easy.
-apply unskolem_equiv; exists i; symmetry; apply inter_full_l; easy.
-(* *)
-destruct Hx as [B [[HB0 HB1] HB2]]; induction HB0 as [i]; auto.
-*)
-Admitted.
+apply (proj1 (is_Basisf_is_Basisp_equiv _ _)).
+Qed.
 
 Variable PB : set_system U.
 
+(* Useful? *)
 Lemma Basisf_of_Basisp : is_Basisp T PB -> is_Basisf T (skolem PB).
 Proof.
-intros [HPB1 HPB2]; split.
-intros i; apply HPB1, skolem_correct; exists i; easy.
-(*
-intros A HA; exists (fun i => incl (skolem PB i) A).
-rewrite (HPB2 _ HA), unionp_any_unionf_any_eq.
-apply set_ext_equiv; split; intros x Hx.
-(* *)
-destruct Hx as [[B HB] Hx]; simpl in Hx.
-exists (exist _ _ (proj1 HB)); split; try easy.
-intros y Hy; simpl in Hy; exists (exist _ B HB); easy.
-(* *)
-destruct Hx as [[B HB] [Hx1 Hx2]]; auto.
-*)
-Admitted.
+apply (proj1 (is_Basisp_is_Basisf_equiv _ _)).
+Qed.
 
 Context {U1 U2 : Type}.
 Variable T1 : set_system U1.