PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lshort mem

St:Type, l:St*, eq:(StSt). (x,y:St. eq(x,y) x = y) (s:St. mem_f(St;s;l) mem_f(St;s;LShort(l)))
By:
GenRepD
THEN
ListInd 2
Generated subgoals:

11. St: Type
2. l: St*
3. eq: StSt
4. x,y:St. eq(x,y) x = y
5. s: St
mem_f(St;s;nil) mem_f(St;s;LShort(nil))
21. St: Type
2. l: St*
3. eq: StSt
4. x,y:St. eq(x,y) x = y
5. s: St
6. u: St
7. v: St*
8. mem_f(St;s;v) mem_f(St;s;LShort(v))
mem_f(St;s;u.v) mem_f(St;s;LShort((u.v)))
31. St: Type
2. l: St*
3. eq: StSt
4. x,y:St. eq(x,y) x = y
5. s: St
mem_f(St;s;LShort(nil)) mem_f(St;s;nil)
41. St: Type
2. l: St*
3. eq: StSt
4. x,y:St. eq(x,y) x = y
5. s: St
6. u: St
7. v: St*
8. mem_f(St;s;LShort(v)) mem_f(St;s;v)
mem_f(St;s;LShort((u.v))) mem_f(St;s;u.v)

About:
alluniverselistfunctionboolimplies
assertapplyequalnilcons