Nuprl Rule : instantiate

!subst(J; subs) ⊢ !subst(C; subs) ext !subst(t; subs)

  BY instantiate subs ()
  
  J  ⊢ ext t


Latex:
!subst(J;  subs)  \mvdash{}  !subst(C;  subs)  ext  !subst(t;  subs)

    BY  instantiate  J  C  subs  ()
   
    J    \mvdash{}  C  ext  t



Date html generated: 2016_12_14-AM-08_53_25
Last ObjectModification: 2016_01_16-PM-07_40_22

Theory : rules


Home Index