(35steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: list exists append lemma 2 1 1 1
1. T: Type
2. P: TProp
3. M: T List
4. L: T List
5. xL.P(x)

x(L @ nil).P(x)
By: RWH (LemmaC Thm* L:T List. (L @ nil) = L) 0
Generated subgoal:

1 xL.P(x)

About:
listnilfunctionuniverseprop

(35steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc