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

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

False xM.P(x)
By:
Choose [2]
THEN
Trivial
Generated subgoals:

None

About:
listfunctionuniverseproporfalse

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