interpretation "append" 'append l1 l2 = (cic:/matita/list/append.con _ l1 l2).
theorem append_nil: \forall A:Set.\forall l:list A.l @ [] = l.
interpretation "append" 'append l1 l2 = (cic:/matita/list/append.con _ l1 l2).
theorem append_nil: \forall A:Set.\forall l:list A.l @ [] = l.