interpretation "cons" 'cons hd tl =
(cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl).
+(* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
+
theorem nil_cons:
\forall A:Set.\forall l:list A.\forall a:A.
a::l <> [].
[ nil => l2
| (cons hd tl) => hd :: append A tl l2 ].
+definition tail := \lambda A:Set. \lambda l: list A.
+ match l with
+ [ nil => []
+ | (cons hd tl) => tl].
+
interpretation "append" 'append l1 l2 = (cic:/matita/list/append.con _ l1 l2).
theorem append_nil: \forall A:Set.\forall l:list A.l @ [] = l.