### Nuprl Lemma : co-w-null_wf

`∀[A:Type]. ∀[w:co-w(A)].  (co-w-null(w) ∈ 𝔹)`

Proof

Definitions occuring in Statement :  co-w-null: `co-w-null(w)` co-w: `co-w(A)` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` guard: `{T}` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` co-w-null: `co-w-null(w)`
Lemmas referenced :  co-w-ext co-w_wf subtype_rel_weakening unit_wf2 equal_wf isl_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry cumulativity isect_memberEquality because_Cache universeEquality applyEquality unionEquality functionEquality independent_isectElimination lambdaFormation dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[A:Type].  \mforall{}[w:co-w(A)].    (co-w-null(w)  \mmember{}  \mBbbB{})

Date html generated: 2018_05_21-PM-10_17_53
Last ObjectModification: 2017_07_26-PM-06_36_28

Theory : bar!induction

Home Index