+(* getFirst *)
+definition get_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ None ?
+ | cons h _ ⇒ Some ? h ].
+
+definition get_first_neList ≝
+λT:Type.λl:ne_list T.match l with
+ [ ne_nil h ⇒ h
+ | ne_cons h _ ⇒ h ].
+
+(* cutFirst *)
+definition cut_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ nil T
+ | cons _ t ⇒ t ].
+
+definition cut_first_neList ≝
+λT:Type.λl:ne_list T.match l with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons _ t ⇒ t ].
+