Nuprl Lemma : param-W_wf

[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].  (pW ∈ P ⟶ Type)


Proof




Definitions occuring in Statement :  param-W: pW uall: [x:A]. B[x] so_apply: x[s1;s2;s3] so_apply: x[s1;s2] so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T param-W: pW so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] implies:  Q prop: pcw-path: Path nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A exists: x:A. B[x] all: x:A. B[x]
Lemmas referenced :  param-co-W_wf all_wf pcw-path_wf pcw-step-agree_wf false_wf le_wf squash_wf exists_wf nat_wf pcw-pp-barred_wf pcw-partial_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality setEquality applyEquality cumulativity because_Cache functionEquality setElimination rename dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation universeEquality

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].
    (pW  \mmember{}  P  {}\mrightarrow{}  Type)



Date html generated: 2016_05_14-AM-06_13_17
Last ObjectModification: 2015_12_26-PM-00_05_38

Theory : co-recursion


Home Index