update in groud_2 and models

[helm.git] / helm / software / matita / nlibrary / arithmetics / R.ma

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 60de71dbd7a2eb6d5fd69a6851603f2bb72dc060..6a74c20540afe66b8409f37f1db51ba6a67273eb 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -231,27 +231,25 @@ nlemma ftcoleqleft:
  #A; #F; #a; #H; ncases H; /2/.
 nqed.
 
-alias symbol "I" (instance 7) = "I".
-alias symbol "I" (instance 18) = "I".
-alias symbol "I" (instance 18) = "I".
-alias symbol "I" (instance 18) = "I".
+(* XXX: disambiguation crazy *)
+alias id "I" = "cic:/matita/ng/topology/igft/I.fix(0,0,2)".
 nlet corec ftfish_coind
  (A: Ax_pro) (F: Ω^A) (P: A → CProp[0])
- (Hcorefl: ∀a. P a → a ∈ F)
- (Hcoleqleft: ∀a. P a → ∀b. a ≤ b → P b)
- (Hcoleqinfinity: ∀a. P a → ∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ P x)
+ (Hcorefl: ∀a:A. P a → a ∈ F)
+ (Hcoleqleft: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → P b)
+ (Hcoleqinfinity: ∀a:A. P a → ∀b:A. pre_r ? (Aleq A) a (*≤*) b → ∀i:I A b. ∃x:A. x ∈ C A b i ↓ {(a)} ∧ P x)
 : ∀a:A. P a → a ⋉ F ≝ ?.
  #a; #H; @
   [ /2/
-  | #b; #H; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); /2/
+  | #b; #H; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); /2/
   | #b; #H1; #i; ncases (Hcoleqinfinity a H ? H1 i); #x; *; #H2; #H3;
-    @ x; @; //; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); //]
+    @ x; @; //; napply (ftfish_coind ??? Hcorefl Hcoleqleft Hcoleqinfinity); //]
 nqed.
 
-(*CSC: non serve manco questo (vedi sotto) *)
+(*CSC: non serve manco questo (vedi sotto) 
 nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A).
  #A; //.
-nqed.
+nqed.*)
 
 alias symbol "I" (instance 6) = "I".
 ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
@@ -277,9 +275,9 @@ ndefinition Q_to_R: Q → Rd.
   | @ [ @ (Qminus q 1) (Qplus q 1) | ncases daemon ]
 ##| #c; #d; #Hc; #Hd; @ [ @ (Qmin (fst … c) (fst … d)) (Qmax (snd … c) (snd … d)) | ncases daemon]
 ##| #a; #H; napply (ftfish_coind Rax ? (λa. fst … a < q ∧ q < snd … a)); /2/
-    [ /5/ | #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
-      [ #w; nnormalize;
-    ##| nnormalize;
-  ]
+    [ ncases daemon; ##| #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
+      [ #w; nnormalize; ncases daemon;
+    ##| nnormalize; ncases daemon;
+##]
 nqed.