(3steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc
At:
all-nsub-add1
n:
, P:(
(n+1)
Prop). (
x:
(n+1). P(x))
P(0) & (
x:
n. P(x+1))
By:
Auto
THEN
EasyHyp
THEN
CaseNat 0 `x'
Generated subgoal:
1
1.
n:
2.
P:
(n+1)
Prop
3.
P(0)
4.
x:
n. P(x+1)
5.
x:
(n+1)
6.
x = 0
P(x)
2
steps
About:
(3steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc
(n+1)
Prop
x:n. P(x+1)(n+1)
x = 0
P(x)
n:, P:((n+1)Prop). (x:(n+1). P(x)) 
P(0) & (x:n. P(x+1))
(n+1)Propx:n. P(x+1)(n+1)x = 0 P(x)
