+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/oplus_4.ma".
-include "ground_2/lib/list2.ma".
-
-(* LISTS OF PAIRS ***********************************************************)
-
-rec definition append2 A1 A2 (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
-[ nil2 ⇒ l2
-| cons2 a1 a2 tl ⇒ {a1, a2} ⨮ append2 A1 A2 tl l2
-].
-
-interpretation "append (list of pairs)"
- 'OPlus A1 A2 l1 l2 = (append2 A1 A2 l1 l2).