X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FFsub%2Futil.ma;h=4f5e1542232f753e7fbb209ecc3fbb0a7ec69760;hb=1ba7566bacd8d29e772646b3c86c7d5c944e9a6e;hp=ac93f8ccf34d87a34db374802bcb18afe4ab2751;hpb=fef5299c2f24e4bed4a6d848a519b0777a28513b;p=helm.git diff --git a/helm/software/matita/library/Fsub/util.ma b/helm/software/matita/library/Fsub/util.ma index ac93f8ccf..4f5e15422 100644 --- a/helm/software/matita/library/Fsub/util.ma +++ b/helm/software/matita/library/Fsub/util.ma @@ -73,7 +73,7 @@ qed. lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t). intros;inversion H;intros - [destruct H2;left;symmetry;assumption + [destruct H2;left;symmetry;reflexivity |destruct H4;right;applyS H1] qed. @@ -112,23 +112,20 @@ theorem append_to_or_in_list: \forall A:Type.\forall x:A. intros 3. elim l [right.apply H - |simplify in H1.inversion H1;intros - [destruct H3.left.rewrite < Hcut. - apply in_Base - |destruct H5. - elim (H l2) - [left.apply in_Skip. - rewrite < H4.assumption - |right.rewrite < H4.assumption - |rewrite > Hcut1.rewrite > H4.assumption + |simplify in H1.inversion H1;intros; destruct; + [left.apply in_Base + | elim (H l2) + [left.apply in_Skip. assumption + |right.assumption + |assumption ] ] ] qed. lemma max_case : \forall m,n.(max m n) = match (leb m n) with - [ false \Rightarrow n - | true \Rightarrow m ]. + [ true \Rightarrow n + | false \Rightarrow m ]. intros;elim m;simplify;reflexivity; qed.