(10steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: unequal termlists 1 1
1. a: Term List
2. b: Term List

termlist_eq(nil;nil) 0 = 0 (i:. i < 0 & nil[i] = nil[i] Term)
By:
RecUnfold `termlist_eq` 0
THEN
Reduce 0
THEN
Analyze 0
THEN
Analyze -1
Generated subgoals:

None

About:
listnilassertnatural_numberless_thanequalimpliesexists

(10steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc