Nuprl Lemma : isinl-member

[T:Type]. ∀[t:Base]. ∀[a,b:T].  if is inl then else b ∈ supposing (t)↓


Proof




Definitions occuring in Statement :  has-value: (a)↓ uimplies: supposing a uall: [x:A]. B[x] isinl: isinl def member: t ∈ T base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a has-value: (a)↓ top: Top prop:
Lemmas referenced :  base_wf top_wf is-exception_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut isinlCases divergentSqle hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin baseClosed hypothesisEquality sqequalRule sqequalAxiom isect_memberEquality because_Cache voidElimination voidEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[t:Base].  \mforall{}[a,b:T].    if  t  is  inl  then  a  else  b  \mmember{}  T  supposing  (t)\mdownarrow{}



Date html generated: 2016_05_13-PM-03_21_58
Last ObjectModification: 2016_01_14-PM-06_47_15

Theory : call!by!value_1


Home Index