Nuprl Rule : lemma_by_obid

H  ⊢ C ext t

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

Latex:
H    \mvdash{}  C  ext  t

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


Date html generated: 2019_06_20-PM-04_11_51
Last ObjectModification: 2015_11_25-PM-03_37_49

Theory : rules


Home Index