From 3c4660604bb23d862c72f64e6b5b5974260eea28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 May 2008 16:34:08 +0000 Subject: [PATCH] case not unfilding fixed --- helm/software/matita/library/decidable_kit/list_aux.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma index 1c79ebc48..a38d5eb83 100644 --- a/helm/software/matita/library/decidable_kit/list_aux.ma +++ b/helm/software/matita/library/decidable_kit/list_aux.ma @@ -65,9 +65,9 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ] [ unfold Not; intros; destruct H1; | simplify; intros; cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H; - [ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1; + [ intro; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1; destruct H; apply H'; reflexivity; - | intros; lapply (IH ? H1) as H'; destruct H; + | intro; lapply (IH ? H1) as H'; destruct H; apply H'; reflexivity;]]]] qed. -- 2.39.2