Nuprl Lemma : grp_sig_wf

GrpSig ∈ 𝕌'


Proof




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

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



Date html generated: 2016_05_15-PM-00_06_12
Last ObjectModification: 2015_12_26-PM-11_47_37

Theory : groups_1


Home Index