From 5a2800676f0a9e2bdfff0645baa131699b26af21 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 1 Mar 2012 13:00:50 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter6.ma | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma index 430fc3f21..cadc0065c 100644 --- a/weblib/tutorial/chapter6.ma +++ b/weblib/tutorial/chapter6.ma @@ -1,6 +1,4 @@ -include "basics/list.ma". -include "basics/sets.ma". -include "basics/deqsets.ma". +include "tutorial/chapter5.ma". definition word ≝ λS:DeqSet.list S. @@ -129,4 +127,3 @@ lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop. (A ∪ {ϵ}) · C =1 A · C ∪ C. #S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l] qed. - -- 2.39.2