Nuprl Rule : extract_by_obid

H  ⊢ t ∈ C

  BY extract_by_obid !parameter{$theorem:o} ()
     
     Let CallLisp(LE-LEMMA-O)
  No Subgoals



Definitions occuring in rule :  equal: t ∈ T axiom: Ax

Latex:
H    \mvdash{}  t  =  t

    BY  extract\_by\_obid  !parameter\{\$theorem:o\}  ()
         
          Let  t  C  =  CallLisp(LE-LEMMA-O)
    No  Subgoals



Date html generated: 2016_12_14-AM-08_53_24
Last ObjectModification: 2015_11_25-PM-03_37_50

Theory : rules


Home Index