### 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: `f a` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` A-null: `A-null(AType)` subtype_rel: `A ⊆r 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