is mentioned by
Thm* x,y:Label. Dec(x = y) | [decidable__equal_lbl] |
Thm* x:Label, ls:Label List. x ls (x ls) | [assert_lbls_member] |
Thm* l1,l2:Label. l1 = l2 l1 = l2 | [eq_lbl_iff] |
Thm* SQType(Label) | [lbl_sq] |
Thm* x,y:Label. lbl_pr( < x, y > ) Label | [lbl_pair_wf2] |
Thm* l1,l2:Label. l1 = l2 l1 = l2 | [assert_eq_label] |
Thm* x:Atom. ptn_atom(x) Label | [ptn_atom_wf3] |
Try larger context: GenAutomata