Nuprl Lemma : cw-step_wf

[A:Type]. ∀[B:A ⟶ Type].  (cw-step(A;a.B[a]) ∈ Type)


Proof




Definitions occuring in Statement :  cw-step: cw-step(A;a.B[a]) uall: [x:A]. B[x] 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 cw-step: cw-step(A;a.B[a]) 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]
Lemmas referenced :  pcw-step_wf unit_wf2 it_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality hypothesisEquality applyEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality cumulativity universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    (cw-step(A;a.B[a])  \mmember{}  Type)



Date html generated: 2016_05_14-AM-06_14_58
Last ObjectModification: 2015_12_26-PM-00_05_16

Theory : co-recursion


Home Index