Nuprl Lemma : tidentity_wf

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


Proof




Definitions occuring in Statement :  tidentity: Id{T} 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 tidentity: Id{T}
Lemmas referenced :  identity_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  universeEquality

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



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

Theory : fun_1


Home Index