Nuprl - Pf hd is member lemma 1 2

1. T: Type
2. eq: {T}
3. L: T List
4. u: T
5. v: T List
6. ||v||1 hd(v)(eq) v

||u.v||1 hd((u.v))(eq) (u.v)

By: Analyze 0 THEN Rewrite (HigherC hd_evalC) 0

Generated subgoal:

1 7. ||u.v||1
u(eq) (u.v)

About: