At:
list all is member lemma
1
1
1
1.
T: Type
2.
eq: {T=
}
3.
eq 
T
T
4.
x,y:T. eq(x,y) 
x = y
5.
P: TProp
6.
L: T List
7.
z: T
xnil.P(x) 
z(eq) nil P(z)
By:
Rewrite (HigherC list_all_unrollC THENC HigherC is_member_unrollC THENC HigherC assert_evalC) 0
Generated subgoals:
None
About:
