X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Ffgraph.ma;h=d22c159d0493c5633d2a01f227d4be5a64f404bb;hb=73a66cce6e72c654fdcd0ce760c405a74af70d08;hp=5b28071dcff455d2cc37d02a3f603861d05842e8;hpb=2c80e9d9409119febcab9c08d6e6cad702384169;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma
index 5b28071dc..d22c159d0 100644
--- a/helm/software/matita/library/decidable_kit/fgraph.ma
+++ b/helm/software/matita/library/decidable_kit/fgraph.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/decidable_kit/fgraph/".
-
 include "decidable_kit/fintype.ma".
 
 definition setA : ∀T:eqType.T → bool := λT,x.true.
@@ -152,7 +150,7 @@ qed.
 lemma mem_concat: 
   ∀d:eqType. ∀x.∀l1,l2:list d.
     mem d x (l1 @ l2) = orb (mem d x l1) (mem d x l2).
-intros; elim l1; [reflexivity] simplify; cases (cmp d x t); simplify; [reflexivity|assumption]
+intros; elim l1; [reflexivity] simplify; cases (cmp d x a); simplify; [reflexivity|assumption]
 qed.
 
 lemma orb_refl : ∀x.orb x x = x. intros (x); cases x; reflexivity; qed. 
@@ -163,7 +161,7 @@ lemma mem_multss :
   match x in list with [ nil ⇒ false | (cons he tl) ⇒ andb (mem ? he s) (mem ? tl l)].
 intros (d s l x); elim s; [cases x] simplify; try reflexivity; rewrite > mem_concat;
 rewrite > H; clear H; rewrite > mem_multes; cases x; simplify; [reflexivity]
-unfold list_eqType; simplify; apply (cmpP ? t s1); intros (E); 
+unfold list_eqType; simplify; apply (cmpP ? a s1); intros (E); 
 cases (mem d s1 l1);
 [1,2: rewrite > E; rewrite > cmp_refl; simplify;
       [rewrite > orb_refl | rewrite > orbC ] reflexivity