---

{ [P:Pi_term]. [t,x:Name]. [avoid:Name List].
    (pi-simple-subst-aux(t;x;P;avoid)  Pi_term) }

{ Proof }

---

Definitions occuring in Statement :  pi-simple-subst-aux: pi-simple-subst-aux(t;x;P;avoid),  pi_term: Pi_term,  name: Name,  uall: [x:A]. B[x],  member: t  T,  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  all: x:A. B[x],  nat: ,  implies: P  Q,  le: A  B,  ge: i  j ,  not: A,  false: False,  prop: ,  pi_term: Pi_term,  pi-rank: pi-rank(p),  pi-simple-subst-aux: pi-simple-subst-aux(t;x;P;avoid),  ycomb: Y,  pizero: 0,  let: let,  picomm: pre.body,  pioption: (left + right),  pipar: (left | right),  pirep: !body,  pinew: (new name. body),  so_lambda: x y.t[x; y],  rev_implies: P  Q,  iff: P  Q,  squash: T,  true: True,  and: P  Q,  unit: Unit,  so_apply: x[s1;s2],  it:
Lemmas :  nat_properties,  ge_wf,  nat_wf,  le_wf,  pi-rank_wf,  name_wf,  pi_term_wf,  pizero_wf,  pi_prefix_ind_wf,  picomm_wf,  pisend_wf,  ifthenelse_wf,  name_eq_wf,  pircv_wf,  maybe-new_wf,  not_wf,  l_member_wf,  pi-replace_wf,  squash_wf,  true_wf,  pi-rank-pi-replace,  pioption_wf,  pipar_wf,  pirep_wf,  pinew_wf

---

\mforall{}[P:Pi\_term].  \mforall{}[t,x:Name].  \mforall{}[avoid:Name  List].    (pi-simple-subst-aux(t;x;P;avoid)  \mmember{}  Pi\_term)


Date html generated: 2011_08_17-PM-06_49_57
Last ObjectModification: 2011_06_18-PM-12_23_22

Home Index