Nuprl Lemma : equal-wf-T-base

[T:Type]. ∀[a:T]. ∀[b:Base].  (a b ∈ T ∈ ℙ)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: member: t ∈ T base: Base universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T prop:
Lemmas referenced :  base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isect_memberEquality isectElimination thin hypothesisEquality because_Cache universeEquality Error :equalityEqualityBase2

Latex:
\mforall{}[T:Type].  \mforall{}[a:T].  \mforall{}[b:Base].    (a  =  b  \mmember{}  \mBbbP{})



Date html generated: 2018_05_21-PM-00_00_02
Last ObjectModification: 2017_11_03-PM-10_11_57

Theory : core_2


Home Index