milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / etc / lib / list.etc

let rec append A (l1: list A) l2 on l1 ≝
  match l1 with
  [ nil        ⇒ l2
  | cons hd tl ⇒ hd :: append A tl l2
  ].

interpretation "append (list)" 'Append l1 l2 = (append ? l1 l2).