+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;
+ [ 1: intro; reflexivity
+ | 2: intros; normalize in H1:(%); destruct H1
+ ].
+qed.
+
+lemma eq_to_isempty : ∀T,l.l = [] → isb_empty_list T l = true.
+ do 2 intro;
+ elim l 0;
+ [ 1: intro; reflexivity
+ | 2: intros; destruct H1
+ ]
+qed.
+