Nuprl Lemma : sqle-wf

[x,y:Base].  (x ≤ y ∈ Type)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] member: t ∈ T base: Base universe: Type sqle: s ≤ t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  base_wf base_sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  hypothesisEquality Error :isect_memberEquality_alt,  isectElimination thin Error :isectIsTypeImplies,  Error :universeIsType,  extract_by_obid sqleIntensionalEquality

Latex:
\mforall{}[x,y:Base].    (x  \mleq{}  y  \mmember{}  Type)



Date html generated: 2019_06_20-AM-11_19_41
Last ObjectModification: 2018_10_15-PM-05_06_54

Theory : sqequal_1


Home Index