Nuprl Lemma : kindcase_wf
∀[B:Type]. ∀[k:Knd]. ∀[f:Id ─→ B]. ∀[g:IdLnk ─→ Id ─→ B]. (kindcase(k;a.f[a];l,t.g[l;t]) ∈ B)
Proof
Definitions occuring in Statement :
kindcase: kindcase(k;a.f[a];l,t.g[l; t]),
Knd: Knd,
IdLnk: IdLnk,
Id: Id,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
function: x:A ─→ B[x],
universe: Type
Lemmas :
IdLnk_wf,
Id_wf,
Knd_wf
\mforall{}[B:Type]. \mforall{}[k:Knd]. \mforall{}[f:Id {}\mrightarrow{} B]. \mforall{}[g:IdLnk {}\mrightarrow{} Id {}\mrightarrow{} B]. (kindcase(k;a.f[a];l,t.g[l;t]) \mmember{} B)
Date html generated:
2015_07_17-AM-09_11_52
Last ObjectModification:
2015_01_28-AM-07_56_54
Home
Index