X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fdecidable_kit%2Ffgraph.ma;h=b2aca796bae2d40db20dab3066a21c68bf6668c0;hb=6ad533c972e6c9e9db53f38f972e7c0792160f2e;hp=cceaa386a4b9c2b3b7e89b9632338aafdb39f85e;hpb=1c12d490ff6ac2005173a695fa1bf4bb561c8066;p=helm.git

diff --git a/matita/library/decidable_kit/fgraph.ma b/matita/library/decidable_kit/fgraph.ma
index cceaa386a..b2aca796b 100644
--- a/matita/library/decidable_kit/fgraph.ma
+++ b/matita/library/decidable_kit/fgraph.ma
@@ -183,7 +183,7 @@ intros 2 (d m); elim m 0; simplify; [intros (x); cases x; reflexivity]
 intros (n IH x); elim x; rewrite > mem_multss; simplify; [reflexivity]
 rewrite > mem_finType; simplify; rewrite > IH; reflexivity;
 qed.
-
+(*
 axiom uniq_concat : ∀d:eqType.∀l1,l2. uniq d (l1@l1) = (andb (uniq ? l1) (andb (uniq ? l2) ())). 
 
 lemma uniq_mkpermr : ∀d:finType.∀m. uniq ? (mkpermr d m) = true.
@@ -261,4 +261,4 @@ Canonical Structure set_finType := FinType (can_uniq can_sval).
 Definition iset_of_fun (f : G -> bool_finType) : setType :=
   locked Sett (fgraph_of_fun f).
 
-
+*)