a,b:Term List. termlist_eq(a;b) 
a = b
Case of b; nil true
; x.xs false ; x.xs Case of b; nil false ; x'.xs' term_eq(x;x')
termlist_eq(xs;xs') (recursive)
is mentioned by
| Thm* a,b:Term List. termlist_eq(a;b) a = b | [assert_termlist_eq] |
Try larger context:
GenAutomata