rec definition list_eq A (l1,l2:list A) on l1 ≝
match l1 with
-[ list_nil ⇒
+[ list_empty ⇒
match l2 with
- [ list_nil ⇒ ⊤
- | list_cons _ _ ⇒ ⊥
+ [ list_empty ⇒ ⊤
+ | list_lcons _ _ ⇒ ⊥
]
-| list_cons a1 l1 ⇒
+| list_lcons a1 l1 ⇒
match l2 with
- [ list_nil ⇒ ⊥
- | list_cons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
+ [ list_empty ⇒ ⊥
+ | list_lcons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
]
].