Simplify proof of is_Basisp_is_Basisf_equiv.

WIP: is_Basisp_equiv.

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -389,16 +389,17 @@ End Trace_Facts.
 
 Section Basis_Facts1.
 
-Context {U Idx : Type}.
+Context {U : Type}.
 
 (** Correctness results. *)
 
 Variable T : set_system U.
 
 Lemma is_Basisf_is_Basisp_equiv :
-  forall (fB : Idx -> set U), is_Basisf T fB <-> is_Basisp T (unskolem fB).
+  forall {Idx : Type} (fB : Idx -> set U),
+    is_Basisf T fB <-> is_Basisp T (unskolem fB).
 Proof.
-intros fB; split; intros [HfB1 HfB2]; split.
+intros Idx fB; split; intros [HfB1 HfB2]; split.
 (* *)
 intros B [i]; easy.
 intros A HA; rewrite (HfB2 A HA) at 1; apply set_ext_equiv; split; intros x.
@@ -414,19 +415,32 @@ Qed.
 Lemma is_Basisp_is_Basisf_equiv :
   forall (PB : set_system U), is_Basisp T PB <-> is_Basisf T (skolem PB).
 Proof.
-intros PB; split; intros [HPB1 HPB2]; split.
-(* *)
-intros [B HB]; auto.
-intros A HA; rewrite (HPB2 A HA) at 1; apply set_ext_equiv; split; intros x.
-intros [B [[HB1 HB2] Hx]]; exists (exist _ _ HB2); easy.
-intros [[B HB] [Hx1 Hx2]]; exists B; easy.
-(* *)
-intros B HB; apply (HPB1 (exist _ _ HB)).
-intros A HA; rewrite (HPB2 A HA) at 1; apply set_ext_equiv; split; intros x.
-intros [[B HB] [Hx1 Hx2]]; exists B; easy.
-intros [B [[HB1 HB2] Hx]]; exists (exist _ _ HB2); easy.
+intros PB; rewrite <- (unskolem_skolem PB) at 1.
+apply iff_sym, is_Basisf_is_Basisp_equiv.
 Qed.
 
+End Basis_Facts1.
+
+
+Section Basis_Facts2.
+
+Context {U : Type}.
+
+Variable T : set_system U.
+
+Lemma is_Basisp_equiv :
+  forall (PB : set_system U),
+    is_Basisp T PB <->
+    (forall A x, T A -> A x -> exists B, PB B /\ incl B A /\ B x).
+Proof.
+intros PB; split.
+(* *)
+intros [HPB1 HPB2] A x HA Hx.
+
+
+
+Admitted.
+
 Variable P : set_system U.
 
 Lemma is_Basisp_Union_any_closure : is_Basisp (Union_any_closure P) P.
@@ -442,10 +456,10 @@ intros y Hy; exists B; easy.
 destruct HB as [HB1 HB2]; auto.
 Qed.
 
-End Basis_Facts1.
+End Basis_Facts2.
 
 
-Section Basis_Facts2.
+Section Basis_Facts3.
 
 Context {U : Type}.
 Variable genU : set_system U.
@@ -475,13 +489,16 @@ admit.
 
 (* . *)
 intros x [i Hx].
+eexists; repeat split.
+admit.
+admit.
 admit.
 
 (* *)
 intros x [B [[HB1 HB2] HB3]]; auto.
 Admitted.
 
-End Basis_Facts2.
+End Basis_Facts3.
 
 
 Section Open_Prod_Facts1.