Nuprl Lemma : rng_sig_wf

RngSig ∈ 𝕌'


Proof




Definitions occuring in Statement :  rng_sig: RngSig member: t ∈ T universe: Type
Definitions unfolded in proof :  rng_sig: RngSig member: t ∈ T
Lemmas referenced :  bool_wf unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productEquality universeEquality cumulativity functionEquality hypothesisEquality cut lemma_by_obid hypothesis unionEquality

Latex:
RngSig  \mmember{}  \mBbbU{}'



Date html generated: 2016_05_15-PM-00_19_58
Last ObjectModification: 2015_12_27-AM-00_03_07

Theory : rings_1


Home Index