Nuprl Rule : cut

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

H J ⊢ T ext (λx.t) s

  BY cut #$i S x

  H J ⊢ S ext s
  H x:S, J ⊢ T ext t

Definitions occuring in rule : apply: f 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: 2019_06_20-PM-04_11_40 Last ObjectModification: 2016_07_08-PM-03_49_01 Theory : rules Home Index