Nuprl Lemma : pi_term_ind_wf_simple
∀[A:Type]. ∀[v:pi_term()]. ∀[zero:A]. ∀[comm:pre:pi_prefix() ─→ body:pi_term() ─→ A ─→ A].
∀[option,par:left:pi_term() ─→ right:pi_term() ─→ A ─→ A ─→ A]. ∀[rep:body:pi_term() ─→ A ─→ A]. ∀[new:name:Name
─→ body:pi_term()
─→ A
─→ A].
(... ∈ A)
Proof
Definitions occuring in Statement :
pi_term_ind: pi_term_ind(v;zero;pre,body,rec1....;left,right,rec2,rec3....;left,right,rec4,rec5....;body,rec6....;name,body,rec7....),
pi_term: pi_term(),
pi_prefix: pi_prefix(),
name: Name,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
member: t ∈ T,
function: x:A ─→ B[x],
universe: Type
Lemmas :
pi_term_ind_wf,
true_wf,
pi_term_wf,
subtype_rel_dep_function,
set_wf,
name_wf,
pi_prefix_wf
Latex:
\mforall{}[A:Type]. \mforall{}[v:pi\_term()]. \mforall{}[zero:A]. \mforall{}[comm:pre:pi\_prefix() {}\mrightarrow{} body:pi\_term() {}\mrightarrow{} A {}\mrightarrow{} A].
\mforall{}[option,par:left:pi\_term() {}\mrightarrow{} right:pi\_term() {}\mrightarrow{} A {}\mrightarrow{} A {}\mrightarrow{} A]. \mforall{}[rep:body:pi\_term() {}\mrightarrow{} A {}\mrightarrow{} A].
\mforall{}[new:name:Name {}\mrightarrow{} body:pi\_term() {}\mrightarrow{} A {}\mrightarrow{} A].
(... \mmember{} A)
Date html generated:
2015_07_23-AM-11_32_51
Last ObjectModification:
2015_01_29-AM-00_54_10
Home
Index