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

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

x(L @ M).P(x)
By: Analyze -1
Generated subgoal:

15. xL.P(x)
6. xM.P(x)
x(L @ M).P(x)

About:
listfunctionuniversepropand

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