let rec all A (R:predicate A) (l:list A) on l ≝
match l with
- [ nil ⇒ True
+ [ nil ⇒ ⊤
| cons hd tl ⇒ R hd ∧ all A R tl
].
let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
[ nil2 ⇒ l2
-| cons2 a1 a2 tl ⇒ {a1, a2} :: append2 A1 A2 tl l2
+| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
].
interpretation "append (list of pairs)"