X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Fmoves.ma;h=c8c3b3478fc865cf53bcd034110e8b2a05fcc9f4;hb=bc02962ed23518a09e7f4ed875d7d967a33de135;hp=6f6d0a67b4b5101f9dab3b5e49b088698b03f9be;hpb=fac3ace96363de48a5fa3d75e2515f1eaf52d133;p=helm.git

diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index 6f6d0a67b..c8c3b3478 100644
--- 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
  ]