Nuprl Rule : instantiate

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

  BY instantiate J C subs ()
  
  J  ⊢ C 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: 2019_06_20-PM-04_11_42
Last ObjectModification: 2016_01_16-PM-07_40_22

Theory : rules


Home Index