Nuprl Rule : isinlCases

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

H  ⊢ C ext !((!\\x.if t is inl then ea else eb) Ax)

  BY isinlCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ inl outl(t)) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is inl then u else v ~ v)) ⊢ C ext eb

Definitions occuring in rule : sqle: s ≤ t, callbyvalue: callbyvalue, natural_number: $n, member: t ∈ T, axiom: Ax, inl: inl x, outl: outl(x), uall: ∀[x:A]. B[x], base: Base, sqequal: s ~ t, isinl: isinl def

Latex:
H \mvdash{} C ext !((!\mbackslash{}\mbackslash{}x.if t is inl then ea else eb) Ax) BY isinlCases x t u v () H \mvdash{} 0 \mleq{} eval x = t in 0 H \mvdash{} t \mmember{} Base H x:(t \msim{} inl outl(t)) \mvdash{} C ext ea H x:(\mforall{}[u,v:Base]. (if t is inl then u else v \msim{} v)) \mvdash{} C ext eb Date html generated: 2019_06_20-PM-04_12_10 Last ObjectModification: 2016_07_08-PM-03_48_53 Theory : rules Home Index