Nuprl Rule : equalityElimination

H x:(p = q ∈ A), J ⊢ C ext t

  BY equalityElimination #$i
  
  H x:(p = q ∈ A), J[Ax/x] ⊢ C[Ax/x] ext t


Definitions occuring in rule :  equal: s = t ∈ T,  axiom: Ax
Latex:
H  x:(p  =  q),  J  \mvdash{}  C  ext  t

    BY  equalityElimination  \#\$i
   
    H  x:(p  =  q),  J[Ax/x]  \mvdash{}  C[Ax/x]  ext  t


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

Theory : rules


Home Index