Nuprl Lemma : identity_wf

[A:Type]. (Id ∈ A ⟶ A)


Proof




Definitions occuring in Statement :  identity: Id 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 identity: Id
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule lambdaEquality hypothesisEquality sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  universeEquality

Latex:
\mforall{}[A:Type].  (Id  \mmember{}  A  {}\mrightarrow{}  A)



Date html generated: 2019_06_20-PM-00_26_13
Last ObjectModification: 2018_09_26-AM-11_48_20

Theory : fun_1


Home Index