Debugging code removed.

[helm.git] / helm / software / matita / library / datatypes / subsets.ma

diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma
index d6bcf4ddacf24944eb92fca355993a8266565c38..7c9a13195f2ba6f07635f3067c5e4e942a07d095 100644 (file)
--- a/helm/software/matita/library/datatypes/subsets.ma
+++ b/helm/software/matita/library/datatypes/subsets.ma
@@ -74,6 +74,14 @@ qed.
 
 interpretation "subseteq" 'subseteq U V = (fun1 ___ (subseteq _) U V).
 
+theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
+ intros 4; assumption.
+qed.
+
+theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
+ intros; apply transitive_subseteq_operator; [apply S2] assumption.
+qed.
+
 definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
  intros;
  constructor 1;
@@ -127,4 +135,4 @@ definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
      [ apply a |4: apply a'] try assumption; apply sym; assumption]
 qed.
 
-interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a).
\ No newline at end of file
+interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a).