From 68d0514bb21f373827bc3578a6b30e5fd95b6271 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Apr 2008 09:23:30 +0000 Subject: [PATCH] removed dummy rewrites --- helm/software/matita/library/list/in.ma | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma index cd372394b..0e3be3a8f 100644 --- a/helm/software/matita/library/list/in.ma +++ b/helm/software/matita/library/list/in.ma @@ -113,8 +113,7 @@ intros 5.elim l [elim (not_in_list_nil ? ? H1) |elim H2 [simplify;rewrite > H;reflexivity - |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;rewrite > H5; - reflexivity]]. + |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;reflexivity]]. qed. lemma in_list_filter_to_p_true : \forall l,x,p. @@ -146,7 +145,7 @@ intros 3;elim l [elim (not_in_list_nil ? ? H) |elim (in_list_cons_case ? ? ? ? H1) [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head - |simplify;apply (bool_elim ? (p t));intro;rewrite > H4;simplify + |simplify;apply (bool_elim ? (p t));intro;simplify; [apply in_list_cons;apply H;assumption |apply H;assumption]]] qed. -- 2.39.2