update in groud_2 and models

[helm.git] / helm / software / matita / library / decidable_kit / fgraph.ma

diff --git a/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma
index 5b28071dcff455d2cc37d02a3f603861d05842e8..d22c159d0493c5633d2a01f227d4be5a64f404bb 100644 (file)
--- 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