]
qed.
+(*
notation > "hvbox(x ∈ l)"
non associative with precedence 30 for @{ 'inlist $x $l }.
notation < "hvbox(x \nbsp ∈ \nbsp l)"
non associative with precedence 30 for @{ 'inlist $x $l }.
-interpretation "item in list" 'inlist x l =
- (cic:/matita/list/in/in_list.ind#xpointer(1/1) _ x l).
+*)
+interpretation "item in list" 'mem x l = (in_list _ x l).
lemma max_case : \forall m,n.(max m n) = match (leb m n) with
[ true \Rightarrow n