From f97f039d5ca79fc8718c08e0f078860e04e86fd0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 8 Sep 2007 22:58:03 +0000 Subject: [PATCH] ... --- helm/software/matita/library/decidable_kit/fgraph.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma index cceaa386a..b2aca796b 100644 --- a/helm/software/matita/library/decidable_kit/fgraph.ma +++ b/helm/software/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). - +*) -- 2.39.2