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

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

ynil.P(y) (x:T. x(eq) nil & P(x))
By: Rewrite (HigherC list_exists_unrollC) 0
Generated subgoals:

None

About:
listnilboolassertapplyfunctionuniverseequal
memberpropimpliesandallexists

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