Nuprl Rule : extract_by_obid
H  ⊢ t = t ∈ C
  BY extract_by_obid !parameter{$theorem:o} ()
     
     Let t C = CallLisp(LE-LEMMA-O)
  No Subgoals
Definitions occuring in rule : 
equal: s = 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:
2019_06_20-PM-04_11_41
Last ObjectModification:
2015_11_25-PM-03_37_50
Theory : rules
Home
Index