Nuprl Lemma : dep-isect-value-type

A:Type. ∀B:A ⟶ Type.  ((value-type(A) ∨ (∀a:A. value-type(B[a])))  value-type(a:A ⋂ B[a]))


Proof




Definitions occuring in Statement :  dep-isect: x:A ⋂ B[x] value-type: value-type(T) so_apply: x[s] all: x:A. B[x] implies:  Q or: P ∨ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q value-type: value-type(T) uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T sq_stable: SqStable(P) so_lambda: λ2x.t[x] so_apply: x[s] has-value: (a)↓ prop: squash: T or: P ∨ Q guard: {T}
Lemmas referenced :  sq_stable__has-value dep-isect_wf equal_wf equal-wf-base base_wf or_wf value-type_wf all_wf value-type-has-value
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry dependent_functionElimination cumulativity sqequalRule lambdaEquality applyEquality functionExtensionality instantiate imageMemberEquality baseClosed imageElimination because_Cache functionEquality universeEquality dependentIntersectionElimination unionElimination independent_isectElimination

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.    ((value-type(A)  \mvee{}  (\mforall{}a:A.  value-type(B[a])))  {}\mRightarrow{}  value-type(a:A  \mcap{}  B[a]))



Date html generated: 2017_10_01-AM-08_39_18
Last ObjectModification: 2017_07_26-PM-04_27_26

Theory : dependent!intersection


Home Index