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

At: list all is member lemma 1 2 1
1. T: Type
2. eq: {T=}
3. eq TT
4. x,y:T. eq(x,y) x = y
5. P: TProp
6. L: T List

(z:T. z(eq) nil P(z)) xnil.P(x)
By: Rewrite (HigherC list_all_unrollC) 0
Generated subgoals:

None

About:
listnilboolassertapplyfunctionuniverseequalmemberpropimpliesall

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