Nuprl Rule : hypothesis_subsumption

H x:A, J ⊢ C ext t

  BY hypothesis_subsumption #$i B ()
  
  H  ⊢ B ⊆r A
  H x:A, J ⊢ x ∈ B
  H x:B, J ⊢ C ext t


Definitions occuring in rule :  subtype_rel: A ⊆r B,  member: t ∈ T,  axiom: Ax
Latex:
H  x:A,  J  \mvdash{}  C  ext  t

    BY  hypothesis\_subsumption  \#\$i  B  ()
   
    H    \mvdash{}  B  \msubseteq{}r  A
    H  x:A,  J  \mvdash{}  x  \mmember{}  B
    H  x:B,  J  \mvdash{}  C  ext  t


Date html generated: 2019_06_20-PM-04_11_51
Last ObjectModification: 2015_11_25-PM-03_46_14

Theory : rules


Home Index