Nuprl Lemma : A-null_wf

[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].  (A-null(AType) ∈ A-map Unit)


Proof




Definitions occuring in Statement :  A-null: A-null(AType) A-map: A-map array-model: array-model(AType) array: array{i:l}(Val;n) nat: uall: [x:A]. B[x] unit: Unit member: t ∈ T apply: a universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T A-null: A-null(AType) subtype_rel: A ⊆B
Lemmas referenced :  A-return_wf unit_wf2 A-map_wf it_wf array_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality equalityTransitivity equalitySymmetry isectEquality universeEquality cumulativity functionEquality axiomEquality isect_memberEquality because_Cache

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].    (A-null(AType)  \mmember{}  A-map  Unit)



Date html generated: 2016_05_15-PM-02_19_16
Last ObjectModification: 2015_12_27-AM-08_58_22

Theory : monads


Home Index