ls == reduce(
a,b. x =
a 
b;false;ls)
l1,l2:Label. l1 = l2 
l1 = l2l1,l2:Label. l1 = l2 
l1 = l2x:Label, ls:Label List. x ls (x ls)x,y:Label. Dec(x = y)| def | lbl | Label == {p:Pattern| ground_ptn(p) } |
| def | lbls_member | x ls == reduce(a,b. x = a b;false;ls) |
| THM | assert_eq_label | l1,l2:Label. l1 = l2 l1 = l2 |
| THM | lbl_sq | SQType(Label) |
| THM | eq_lbl_iff | l1,l2:Label. l1 = l2 l1 = l2 |
| THM | assert_lbls_member | x:Label, ls:Label List. x ls (x ls) |
| THM | decidable__equal_lbl | x,y:Label. Dec(x = y) |