Nuprl Rule : applyInr
This rule proved as lemma rule_apply_inr_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ (inr a ) b ≤ ⊥
BY applyInr ()
No Subgoals
Definitions occuring in rule :
sqle: s ≤ t,
apply: f a,
inr: inr x ,
bottom: ⊥,
axiom: Ax
Latex:
H \mvdash{} (inr a ) b \mleq{} \mbot{}
BY applyInr ()
No Subgoals
Date html generated:
2019_06_20-PM-04_12_19
Last ObjectModification:
2016_07_08-PM-03_49_07
Theory : rules
Home
Index