Add Lift_Lift_full.

Use new API (Trace and Lift are images).
Renaming: V -> A (set on which the trace is taken).

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -341,10 +341,15 @@ Section Subset_Lift_Trace_Facts.
 Context {U : Type}.
 Variable A : set U.
 
+Lemma Lift_Lift_full : forall (PA : subset_system A), Incl (Lift A PA) (Lift_full A PA).
+Proof.
+intros PA B [BA HBA]; unfold Lift_full; rewrite trace_lift; easy.
+Qed.
+
 Lemma Lift_Trace_equiv :
   forall (P : set_system U), P A <-> Lift A (Trace A P) = Subset A P.
 Proof.
-split; intros H.
+intros P; split; intros HP.
 (* *)
 apply Ext_equiv; split; intros B HB.
 apply Sub.
@@ -354,9 +359,12 @@ Admitted.
 
 Lemma Trace_Lift : forall (PA : subset_system A), Trace A (Lift A PA) = PA.
 Proof.
-apply Ext_equiv; split; intros B HB.
-induction HB as [B HB]; easy.
-rewrite <- trace_lift in *; easy.
+intros PA; apply Ext_equiv; split; intros BA HBA.
+(* *)
+induction HBA as [B HB]; unfold Lift, liftp_any in HB; rewrite image_eq in HB.
+destruct HB as [BA [HBA1 HBA2]]; rewrite HBA2, trace_lift; easy.
+(* *)
+rewrite <- trace_lift; easy.
 Qed.
 
 Lemma Trace_equiv : forall (P : set_system U) B, Trace A P B <-> exists C, P C /\ B = trace A C.
@@ -370,9 +378,9 @@ Lemma Lift_Incl_Incl_Trace :
   forall (PA : subset_system A) (P : set_system U),
     Incl (Lift A PA) P -> Incl PA (Trace A P).
 Proof.
-intros HPA B HB.
+intros PA P HPA B HB.
 apply Trace_equiv; exists (lift A B); split.
-apply HPA; unfold Lift; rewrite trace_lift; easy.
+apply HPA; easy.
 rewrite trace_lift; easy.
 Qed.
 
@@ -452,42 +460,42 @@ End Image_Preimage_Facts2.
 Section Trace_Facts.
 
 Context {U : Type}.
+Variable A : set U.
 Variable P : set_system U.
-Variable V : set U.
 
-Lemma Trace_wEmpty : wEmpty P -> wEmpty (Trace V P).
+Lemma Trace_wEmpty : wEmpty P -> wEmpty (Trace A P).
 Proof.
 intros; unfold wEmpty; rewrite <- trace_emptyset_r; easy.
 Qed.
 
-Lemma Trace_wFull : wFull P -> wFull (Trace V P).
+Lemma Trace_wFull : wFull P -> wFull (Trace A P).
 Proof.
 intros; unfold wFull; rewrite <- trace_fullset_r; easy.
 Qed.
 
-Lemma Trace_Compl : Compl P -> Compl (Trace V P).
+Lemma Trace_Compl : Compl P -> Compl (Trace A P).
 Proof.
-intros HP A [B HB]; rewrite <- trace_compl; apply Tr; auto.
+intros HP _ [B HB]; rewrite <- trace_compl; apply Im; auto.
 Qed.
 
-Lemma Trace_Diff : Diff P -> Diff (Trace V P).
+Lemma Trace_Diff : Diff P -> Diff (Trace A P).
 Proof.
-intros HP A1 A2 [B1 HB1] [B2 HB2]; rewrite <- trace_diff; apply Tr, HP; auto.
+intros HP _ _ [B1 HB1] [B2 HB2]; rewrite <- trace_diff; apply Im, HP; auto.
 Qed.
 
-Lemma Trace_Sym_diff : Sym_diff P -> Sym_diff (Trace V P).
+Lemma Trace_Sym_diff : Sym_diff P -> Sym_diff (Trace A P).
 Proof.
-intros HP A1 A2 [B1 HB1] [B2 HB2]; rewrite <- trace_sym_diff; apply Tr; auto.
+intros HP _ _ [B1 HB1] [B2 HB2]; rewrite <- trace_sym_diff; apply Im; auto.
 Qed.
 
-Lemma Trace_Inter : Inter P -> Inter (Trace V P).
+Lemma Trace_Inter : Inter P -> Inter (Trace A P).
 Proof.
-intros HP A1 A2 [B1 HB1] [B2 HB2]; rewrite <- trace_inter; apply Tr, HP; auto.
+intros HP _ _ [B1 HB1] [B2 HB2]; rewrite <- trace_inter; apply Im, HP; auto.
 Qed.
 
-Lemma Trace_Union : Union P -> Union (Trace V P).
+Lemma Trace_Union : Union P -> Union (Trace A P).
 Proof.
-intros HP A1 A2 [B1 HB1] [B2 HB2]; rewrite <- trace_union; apply Tr, HP; auto.
+intros HP _ _ [B1 HB1] [B2 HB2]; rewrite <- trace_union; apply Im, HP; auto.
 Qed.
 
 End Trace_Facts.