Nuprl Rule : sqequalRule

H  ⊢ a ~ b ext t

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


Definitions occuring in rule :  sqequal: s ~ t
Latex:
H    \mvdash{}  a  \msim{}  b  ext  t

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


Date html generated: 2019_06_20-PM-04_11_42
Last ObjectModification: 2015_11_24-PM-01_52_02

Theory : rules


Home Index