Nuprl Lemma : test3
λloc,L. loc ∈ ⋂A1,B1:Type. (B1 ⟶ A1 ⟶ B1)
Proof
Definitions occuring in Statement :
member: t ∈ T,
lambda: λx.A[x],
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
member: t ∈ T
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberEquality,
lambdaEquality,
hypothesisEquality,
universeEquality
Latex:
\mlambda{}loc,L. loc \mmember{} \mcap{}A1,B1:Type. (B1 {}\mrightarrow{} A1 {}\mrightarrow{} B1)
Date html generated:
2016_05_15-PM-07_46_34
Last ObjectModification:
2015_12_27-AM-11_09_22
Theory : general
Home
Index