Nuprl - Proof: assert l ball 1

(7steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: assert l ball 1

1. T: Type
2. L: T List
3. u: T
4. v: T List
5. P:(T). (xv.P(x)) (i:||v||. P(v[i]))
6. P: T
7. P(u)
8. (xv.P(x))
9. i: (||v||+1)

P([u / v][i])

By: InstHyp [P] 5 THEN ThinTrivial THEN CaseNat 0 `i' THEN Reduce 0

Generated subgoal:

1 10. (xv.P(x)) (i:||v||. P(v[i]))
11. i:||v||. P(v[i])
12. i = 0
P([u / v][i]) 1 step

About:

(7steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc