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

At: list all append lemma 2 1 2 1
1. T: Type
2. P: TProp
3. L: T List
4. u: T
5. v: T List
6. xv.P(x) (M:T List. xM.P(x) x(v @ M).P(x))
7. P(u)
8. xv.P(x)
9. M: T List
10. xM.P(x)

x(v @ M).P(x)
By: HypBackchain
Generated subgoals:

None

About:
listfunctionuniversepropimpliesall

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