{ 
[v:Name]. [P:Pi_term]. (pi-rank((new v. P)) = (pi-rank(P) + 1)) }
{ Proof }
Definitions occuring in Statement :
pi-rank: pi-rank(p),
pinew: (new name. body),
pi_term: Pi_term,
name: Name,
nat: 
,
uall: [x:A]. B[x],
add: n + m,
natural_number: $n,
equal: s = t
Definitions :
uall: [x:A]. B[x],
pi-rank: pi-rank(p),
member: t 
T,
nat:
Lemmas :
pi-rank_wf,
nat_wf,
pi_term_wf,
name_wf
\mforall{}[v:Name]. \mforall{}[P:Pi\_term]. (pi-rank((new v. P)) = (pi-rank(P) + 1))
Date html generated:
2011_08_17-PM-06_48_09
Last ObjectModification:
2011_06_18-PM-12_20_22
Home
Index