Nuprl Rule : cut

This rule proved as lemma rule_cut_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq  

J ⊢ ext x.t) s

  BY cut #$i x
  
  J ⊢ ext s
  x:S, J ⊢ ext t



Definitions occuring in rule :  apply: a lambda: λx.A[x]

Latex:
H  J  \mvdash{}  T  ext  (\mlambda{}x.t)  s

    BY  cut  \#\$i  S  x
   
    H  J  \mvdash{}  S  ext  s
    H  x:S,  J  \mvdash{}  T  ext  t



Date html generated: 2016_12_14-AM-08_53_23
Last ObjectModification: 2016_07_08-PM-03_49_01

Theory : rules


Home Index