Many axioms are now proved... using many more (but simpler) axioms.

[helm.git] / helm / software / matita / contribs / assembly / compiler / utility.ma

diff --git a/helm/software/matita/contribs/assembly/compiler/utility.ma b/helm/software/matita/contribs/assembly/compiler/utility.ma
index c67298d390673fe02d0519d1241ed2e84a389133..014d598df0c5ad4ae6b16c2b161f756282bd260f 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/utility.ma
+++ b/helm/software/matita/contribs/assembly/compiler/utility.ma
@@ -198,6 +198,21 @@ lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empt
    normalize; autobatch ]
 qed.
 
+definition isnot_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
+
+definition isnotb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
+
+lemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
+ unfold isnotb_empty_list;
+ unfold isnot_empty_list;
+ intros;
+ elim l;
+ [ normalize; autobatch |
+   normalize; autobatch ]
+qed.
+
 lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = [].
  do 2 intro;
  elim l 0;