Nuprl Rule : sqleRule

H  ⊢ a ≤ b ext t

  BY sqle ()
     
     Let SubGoals t = CallLisp(SQLE)
  SubGoals


Definitions occuring in rule :  sqle: s ≤ t
Latex:
H    \mvdash{}  a  \mleq{}  b  ext  t

    BY  sqle  ()
         
          Let  SubGoals  t  =  CallLisp(SQLE)
    SubGoals


Date html generated: 2019_06_20-PM-04_12_00
Last ObjectModification: 2015_11_24-PM-01_52_03

Theory : rules


Home Index