At:
list all iff assert list all 2
2
2
1.
T: Type
2.
L: T List
3.
P: T
4.
u: T
5.
v: T List
6.
x
v.P(x) 
xv.P(x)
x(u.v).P(x) x(u.v).P(x)
By:
Rewrite (HigherC list_all_2_unrollC THENC HigherC list_all_unrollC) 0
Generated subgoals:
| 1 | 7. P(u) xv.P(x)
P(u) |
| 2 | 7. P(u)xv.P(x)
xv.P(x) |
About:
