Nuprl Lemma : church-pair_wf

[A,B,C:Type].  (church-pair() ∈ A ⟶ B ⟶ (A ⟶ B ⟶ C) ⟶ C)


Proof




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

Latex:
\mforall{}[A,B,C:Type].    (church-pair()  \mmember{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  (A  {}\mrightarrow{}  B  {}\mrightarrow{}  C)  {}\mrightarrow{}  C)



Date html generated: 2016_05_15-PM-03_22_16
Last ObjectModification: 2015_12_27-PM-01_04_43

Theory : general


Home Index