even more polymorphic dualizer

[helm.git] / helm / software / matita / contribs / dama / dama / lebesgue.ma

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 5957235ccc183793c5c1e1a209c9f4ca1ecc4de5..1536476b09c0a91e22e9c3f87570dc58a6b54f7f 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -59,14 +59,6 @@ cases (wloss_prop (os_l C))(W W); unfold os_r; unfold dual_hos; simplify;rewrite
   rewrite <W in H1; simplify in H1; apply (H1 Hw);]
 qed. 
 
-alias symbol "upp" = "uppper".
-alias symbol "leq" = "Ordered set less or equal than".
-lemma cases_in_segment: 
-  ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → seg_l C s (λl.l ≤≤ x) ∧ seg_u C s (λu.x ≤≤ u).
-intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
-cases H; split; assumption;
-qed. 
-
 lemma trans_under_upp:
  ∀O:ordered_set.∀s:‡O.∀x,y:O.
   x ≤ y → 𝕦_s (λu.y ≤ u) → 𝕦_s (λu.x ≤ u).