(4steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: append nil right identity 1 2
1. T: Type
2. L: T List
3. u: T
4. v: T List
5. (v @ nil) = v

u.(v @ nil) = u.v
By: HypSubst -1 0
Generated subgoals:

None

About:
listconsniluniverseequal

(4steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc