Nuprl Lemma : sqequal_n_wf

[x,y:Base]. ∀[n:ℕ].  (x ~n y ∈ Type)


Proof




Definitions occuring in Statement :  nat: uall: [x:A]. B[x] member: t ∈ T base: Base universe: Type sqequal_n: ~n t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  sqequal_n-wf nat_wf base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

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



Date html generated: 2016_05_13-PM-04_03_34
Last ObjectModification: 2015_12_26-AM-10_56_13

Theory : int_1


Home Index