even more polymorphic dualizer

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

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 2a1089fec45188916b69bfd8659df83030afcf49..56b354859ad2521bc94a30f458adf29b3b3ad72e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -27,14 +27,14 @@ interpretation "" ' = ( (os_r _)).
 (* Definition 2.1 *)
 record half_ordered_set: Type ≝ {
   hos_carr:> Type;
-  wloss: ∀A:Type. (A → A → CProp) → A → A → CProp;
-  wloss_prop: (∀T,P,x,y.P x y = wloss T P x y) ∨ (∀T,P,x,y.P y x = wloss T P x y); 
+  wloss: ∀A,B:Type. (A → A → B) → A → A → B;
+  wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y); 
   hos_excess_: hos_carr → hos_carr → CProp;
-  hos_coreflexive: coreflexive ? (wloss ? hos_excess_);
-  hos_cotransitive: cotransitive ? (wloss ? hos_excess_)
+  hos_coreflexive: coreflexive ? (wloss ?? hos_excess_);
+  hos_cotransitive: cotransitive ? (wloss ?? hos_excess_)
 }.
 
-definition hos_excess ≝ λO:half_ordered_set.wloss O ? (hos_excess_ O). 
+definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O). 
 
 (*
 lemma find_leq : half_ordered_set → half_ordered_set.
@@ -55,7 +55,7 @@ qed.
 definition dual_hos : half_ordered_set → half_ordered_set.
 intro; constructor 1;
 [ apply (hos_carr h);
-| apply (λT,f,x,y.wloss h T f y x); 
+| apply (λT,R,f,x,y.wloss h T R f y x); 
 | intros; cases (wloss_prop h);[right|left]intros;apply H; 
 | apply (hos_excess_ h);
 | apply (hos_coreflexive h);
@@ -169,12 +169,12 @@ apply (mk_half_ordered_set (O × O));
 [1: apply (wloss O);
 |2: intros; cases (wloss_prop O); [left|right] intros; apply H;
 |3: apply (square_exc O); 
-|4: intro x; cases (wloss_prop O); rewrite < (H  ? (square_exc O) x x); clear H;
+|4: intro x; cases (wloss_prop O); rewrite < (H  ?? (square_exc O) x x); clear H;
     cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
     [1,3: apply (hos_coreflexive O h H1);
     |*: apply (hos_coreflexive O h1 H1);]
 |5: intros 3 (x0 y0 z0); cases (wloss_prop O);
-    do 3 rewrite < (H  ? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
+    do 3 rewrite < (H  ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
     simplify; intro H; cases H; clear H;
     [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
     |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;