Nuprl Rule : sqequalRule

H  ⊢ ext t

  BY sqequal ()
     
     Let SubGoals CallLisp(SQEQ)
  SubGoals



Definitions occuring in rule :  sqequal: t

Latex:
H    \mvdash{}  a  \msim{}  b  ext  t

    BY  sqequal  ()
         
          Let  SubGoals  t  =  CallLisp(SQEQ)
    SubGoals



Date html generated: 2016_12_14-AM-08_53_25
Last ObjectModification: 2015_11_24-PM-01_52_02

Theory : rules


Home Index