{ 
[p:Pi_term]. (pi-subst-aux(p) 
Name List 
(Name 
Name) List Pi_term) }
{ Proof }
Definitions occuring in Statement :
pi-subst-aux: pi-subst-aux(p),
pi_term: Pi_term,
name: Name,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
pi-subst-aux: pi-subst-aux(p),
let: let,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_lambda: 
x y.t[x; y],
top: Top,
all: x:A. B[x],
subtype: S 
T,
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
prop: 
Lemmas :
pi_term_ind_wf,
name_wf,
pi_term_wf,
pizero_wf,
pi_prefix_ind_wf,
picomm_wf,
pisend_wf,
name-subst_wf,
ifthenelse_wf,
deq-member_wf,
name-deq_wf,
pircv_wf,
filter_wf,
bnot_wf,
name_eq_wf,
pi1_wf_top,
maybe-new_wf,
append_wf,
pi-names_wf,
not_wf,
l_member_wf,
pi_prefix_wf,
pioption_wf,
pipar_wf,
pirep_wf,
pinew_wf
\mforall{}[p:Pi\_term]. (pi-subst-aux(p) \mmember{} Name List {}\mrightarrow{} (Name \mtimes{} Name) List {}\mrightarrow{} Pi\_term)
Date html generated:
2011_08_17-PM-06_49_45
Last ObjectModification:
2011_06_18-PM-12_23_06
Home
Index