Nuprl Lemma : atom2_sq

SQType(Atom2)


Proof




Definitions occuring in Statement :  atom: Atom$n sq_type: SQType(T)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a
Lemmas referenced :  subtype_base_sq atom2_subtype_base
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin atomnEquality independent_isectElimination hypothesis

Latex:
SQType(Atom2)



Date html generated: 2016_05_13-PM-03_21_08
Last ObjectModification: 2015_12_26-AM-09_12_07

Theory : atom_1


Home Index