Nuprl Lemma : interval-groupoid_wf

interval-groupoid() ∈ Groupoid


Proof




Definitions occuring in Statement :  interval-groupoid: interval-groupoid() groupoid: Groupoid member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T interval-groupoid: interval-groupoid()
Lemmas referenced :  int_seg_wf tree-groupoid_wf
Rules used in proof :  hypothesis natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

Latex:
interval-groupoid()  \mmember{}  Groupoid



Date html generated: 2017_10_05-AM-00_49_09
Last ObjectModification: 2017_10_02-PM-05_18_54

Theory : small!categories


Home Index