mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly2 / universe / universe.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/universe/universe.ma b/helm/software/matita/contribs/ng_assembly2/universe/universe.ma
old mode 100755 (executable)
new mode 100644 (file)
index 24e5e5a..71eec78
--- a/helm/software/matita/contribs/ng_assembly2/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly2/universe/universe.ma
@@ -88,7 +88,7 @@ nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
  #u1; #dim1;
  #y; nelim y;
  #u2; #dim2;
- nchange with (? → eqc ? u1 u2 = true);
+ nchange with (? → (eqc ? u1 u2) = true);
  #H; napply (eq_to_eqc ? u1 u2);
  napply (SUN_destruct_1 l … H).
 nqed.
@@ -108,7 +108,7 @@ naxiom eqSUN_to_eq_aux : ∀l,x,y.((getelem l x) = (getelem l y)) → x = y.
 
 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #l; #x; #y;
- nchange with ((eqc ? (getelem ? x) (getelem ? y) = true) → x = y);
+ nchange with (((eqc ? (getelem ? x) (getelem ? y)) = true) → x = y);
  #H; napply (eqSUN_to_eq_aux l x y (eqc_to_eq … H)).
 nqed.
 
@@ -147,7 +147,7 @@ nlet rec farg1_auxT (T:Type) (l:ne_list nat) on l ≝
   | ne_cons _ t ⇒ ProdT T (farg1_auxT T t)
   ].
 
-nlemma farg1_auxDim : ∀h,t,x.eqc ? x h = false → member_natList x (h§§t) = true → member_natList x t = true.
+nlemma farg1_auxDim : ∀h,t,x.(eqc ? x h) = false → member_natList x (h§§t) = true → member_natList x t = true.
  #h; #t; #x; #H; #H1;
  nnormalize in H1:(%);
  nrewrite > H in H1:(%);
@@ -160,10 +160,10 @@ nlet rec farg1 (T:Type) (l:ne_list nat) on l ≝
   [ ne_nil h ⇒ λarg:farg1_auxT T «£h».λx:S_UN «£h».arg
   | ne_cons h t ⇒ λarg:farg1_auxT T (h§§t).λx:S_UN (h§§t).
    match eqc ? (getelem ? x) h
-    return λy.eqc ? (getelem ? x) h = y → ?
+    return λy.(eqc ? (getelem ? x) h) = y → ?
    with
-    [ true ⇒ λp:(eqc ? (getelem ? x) h = true).fst … arg
-    | false ⇒ λp:(eqc ? (getelem ? x) h = false).
+    [ true ⇒ λp:((eqc ? (getelem ? x) h) = true).fst … arg
+    | false ⇒ λp:((eqc ? (getelem ? x) h) = false).
      farg1 T t
       (snd … arg)
       (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
@@ -176,10 +176,10 @@ nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝
   [ ne_nil h ⇒ λarg:farg1_auxT (farg1_auxT T lfix) «£h».λx:S_UN «£h».farg1 T lfix arg
   | ne_cons h t ⇒ λarg:farg1_auxT (farg1_auxT T lfix) (h§§t).λx:S_UN (h§§t).
    match eqc ? (getelem ? x) h
-    return λy.eqc ? (getelem ? x) h = y → ?
+    return λy.(eqc ? (getelem ? x) h) = y → ?
    with
-    [ true ⇒ λp:(eqc ? (getelem ? x) h = true).farg1 T lfix (fst … arg)
-    | false ⇒ λp:(eqc ? (getelem ? x) h = false).
+    [ true ⇒ λp:((eqc ? (getelem ? x) h) = true).farg1 T lfix (fst … arg)
+    | false ⇒ λp:((eqc ? (getelem ? x) h) = false).
      farg2 T t lfix
       (snd … arg)
       (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))