{ 
[t,x:Name]. [P:Pi_term]. (pi-level(pi-replace(t;x;P)) = pi-level(P)) }
{ Proof }
Definitions occuring in Statement :
pi-replace: pi-replace(t;x;P),
pi-level: pi-level(p),
pi_term: Pi_term,
name: Name,
uall: [x:A]. B[x],
int: 
,
equal: s = t
Definitions :
uall: [x:A]. B[x],
pi-level: pi-level(p),
pi-replace: pi-replace(t;x;P),
member: t 
T,
all: x:A. B[x],
prop: 
,
implies: P 
Q,
so_lambda: 
x.t[x],
squash: 
T,
true: True,
and: P 
Q,
let: let,
so_apply: x[s],
guard: {T},
nat: 
Lemmas :
pi_term-induction,
pi-level_wf,
pi-replace_wf,
nat_wf,
pi_prefix_wf,
pi_term_wf,
name_wf,
imax_wf,
squash_wf,
true_wf
\mforall{}[t,x:Name]. \mforall{}[P:Pi\_term]. (pi-level(pi-replace(t;x;P)) = pi-level(P))
Date html generated:
2011_08_17-PM-06_49_17
Last ObjectModification:
2011_06_18-PM-12_22_18
Home
Index