Removed duplicated notation and interaction with the user.

diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
index a8ee13a074ad558fbd733c1f2b7718a9d0177c96..85f4ef3ba24264bc6d284c77c5f87518beda2344 100644 (file)
--- a/matita/matita/lib/basics/finset.ma
+++ b/matita/matita/lib/basics/finset.ma
@@ -102,6 +102,8 @@ definition FinSum ≝ λA,B:FinSet.
    (enum_sum A B (enum A) (enum B)) 
    (enumAB_unique … (enum_unique A) (enum_unique B)).
 
+include alias "basics/types.ma".
+
 unification hint  0 ≔ C1,C2; 
     T1 ≟ FinSetcarr C1,
     T2 ≟ FinSetcarr C2,

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index e46f45f075416af0fd6b58c18fe2695e2da61515..7951f2997265484adf6ec17130e2148f9f043420 100644 (file)
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -31,8 +31,7 @@ let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
   | cons a tl ⇒ (x == a) ∨ memb S x tl
   ].
 
-notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
-interpretation "boolean membership" 'memb a l = (memb ? a l).
+interpretation "boolean membership" 'mem a l = (memb ? a l).
 
 lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
 #S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //

diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index 6f6d0a67b4b5101f9dab3b5e49b088698b03f9be..c8c3b3478fc865cf53bcd034110e8b2a05fcc9f4 100644 (file)
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -92,8 +92,7 @@ theorem move_ok:
    (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ a::w∈\sem{i2} *)
    @iff_trans[||@(iff_or_l … (HI2 w))] 
    (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ w∈\sem{move S a i2} *)
-   @iff_or_r 
-   check deriv_middot 
+   @iff_or_r
    (* we are left to prove that 
      w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
      we use deriv_middot on the rhs *)
@@ -145,7 +144,6 @@ theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
 #S #w elim w 
  [* #i #b >moves_empty cases b % /2/
  |#a #w1 #Hind #e >moves_cons
- check not_epsilon_sem
   @iff_trans [||@iff_sym @not_epsilon_sem]
   @iff_trans [||@move_ok] @Hind
  ]