### Nuprl Lemma : church-null_wf

`∀[A,T:Type].  (church-null() ∈ ((Top ⟶ Top ⟶ Top ⟶ T ⟶ T) ⟶ A) ⟶ A)`

Proof

Definitions occuring in Statement :  church-null: `church-null()` uall: `∀[x:A]. B[x]` top: `Top` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` church-null: `church-null()`
Lemmas referenced :  church-false_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality applyEquality hypothesisEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis functionEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[A,T:Type].    (church-null()  \mmember{}  ((Top  {}\mrightarrow{}  Top  {}\mrightarrow{}  Top  {}\mrightarrow{}  T  {}\mrightarrow{}  T)  {}\mrightarrow{}  A)  {}\mrightarrow{}  A)

Date html generated: 2016_05_15-PM-03_22_34
Last ObjectModification: 2015_12_27-PM-01_05_01

Theory : general

Home Index