...

[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 a024ada3d031b259fc823128bfbbaa16150067f8..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.
@@ -35,7 +33,7 @@ apply prove_reflect; intros;
  [1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2); 
      intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType));
      reflexivity
- |2: unfold Not; intros (H3); destruct H3; rewrite > Hcut in H2;
+ |2: unfold Not; intros (H3); destruct H3;
      rewrite > (cmp_refl (list_eqType d2)) in H2; destruct H2;]
 qed.
 
@@ -140,7 +138,7 @@ definition mkpermr :=
 lemma mem_multes : 
   ∀d:finType.∀e:d.∀l:list_eqType (list_eqType d).∀s:list_eqType d.
   mem ? s (multes ? e l) = 
-  match s in list with [ Nil ⇒ false | (Cons e1 tl) ⇒ andb (cmp ? e e1) (mem ? tl l)].
+  match s in list with [ nil ⇒ false | (cons e1 tl) ⇒ andb (cmp ? e e1) (mem ? tl l)].
 intros (d e l s); elim l (hd tl IH); [cases s;simplify;[2: rewrite > andbC] reflexivity]
 simplify; rewrite > IH; cases s; simplify; [reflexivity]
 unfold list_eqType; simplify;
@@ -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. 
@@ -160,10 +158,10 @@ lemma orb_refl : ∀x.orb x x = x. intros (x); cases x; reflexivity; qed.
 lemma mem_multss : 
   ∀d:finType.∀s:list_eqType d.∀l:list_eqType (list_eqType d).∀x:list_eqType d.
   mem ? x (multss ? s l) = 
-  match x in list with [ Nil ⇒ false | (Cons he tl) ⇒ andb (mem ? he s) (mem ? tl l)].
+  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