From: Enrico Tassi Date: Thu, 8 Nov 2007 14:54:31 +0000 (+0000) Subject: ported to the new destruct X-Git-Tag: 0.4.95@7852~35 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b76f72834c3885d06ceb71d92bf53e5d6334b24a;p=helm.git ported to the new destruct --- diff --git a/matita/library/decidable_kit/eqtype.ma b/matita/library/decidable_kit/eqtype.ma index 88721632f..35f404df3 100644 --- a/matita/library/decidable_kit/eqtype.ma +++ b/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/matita/library/decidable_kit/list_aux.ma b/matita/library/decidable_kit/list_aux.ma index c1a03060b..33a57c752 100644 --- a/matita/library/decidable_kit/list_aux.ma +++ b/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.