From d4b7b23a0627c97315dc454c8193ce082f00b249 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 8 Nov 2007 14:54:31 +0000 Subject: [PATCH] ported to the new destruct --- helm/software/matita/library/decidable_kit/eqtype.ma | 5 ++--- helm/software/matita/library/decidable_kit/list_aux.ma | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma index 88721632f..35f404df3 100644 --- a/helm/software/matita/library/decidable_kit/eqtype.ma +++ b/helm/software/matita/library/decidable_kit/eqtype.ma @@ -95,7 +95,7 @@ cases x (s ps); cases y (t pt); simplify; intros (Est); [1: constructor 1; generalize in match ps; rewrite > Est; intros (pt'); rewrite < (pirrel ? ? ? pt pt' (eqType_decidable bool_eqType)); reflexivity; |2: constructor 2; unfold Not; intros (H); destruct H; - cases (Est); assumption;] + cases (Est); reflexivity] qed. definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p). @@ -132,8 +132,7 @@ cases a; cases b; simplify; intros (H); |2,3,5: destruct H; |4: rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; |6,7: unfold Not; intros (H1); destruct H1 -|8: unfold Not; intros (H1); destruct H1; - rewrite > Hcut in H; rewrite > cmp_refl in H; destruct H;] +|8: unfold Not; intros (H1); destruct H1;rewrite > cmp_refl in H; destruct H;] qed. definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d). diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma index c1a03060b..33a57c752 100644 --- a/helm/software/matita/library/decidable_kit/list_aux.ma +++ b/helm/software/matita/library/decidable_kit/list_aux.ma @@ -96,7 +96,7 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ] | simplify; intros; cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H; [ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1; - destruct H; rewrite > Hcut in H'; apply H'; reflexivity; + destruct H; apply H'; reflexivity; | intros; lapply (IH ? H1) as H'; destruct H; apply H'; reflexivity;]]]] qed. -- 2.39.2