Nuprl Lemma : omon_wf

OMon ∈ 𝕌'


Proof




Definitions occuring in Statement :  omon: OMon member: t ∈ T universe: Type
Definitions unfolded in proof :  omon: OMon member: t ∈ T and: P ∧ Q uall: [x:A]. B[x] abmonoid: AbMon mon: Mon so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] subtype_rel: A ⊆B prop: all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt band: p ∧b q ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a bfalse: ff infix_ap: y
Lemmas referenced :  abmonoid_wf ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity setEquality cut introduction extract_by_obid hypothesis productEquality sqequalHypSubstitution isectElimination thin setElimination rename because_Cache sqequalRule lambdaEquality hypothesisEquality applyEquality cumulativity universeEquality instantiate functionEquality lambdaFormation unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination

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



Date html generated: 2017_10_01-AM-08_14_19
Last ObjectModification: 2017_02_28-PM-01_58_38

Theory : groups_1


Home Index