### Nuprl Lemma : isinl-member

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

Proof

Definitions occuring in Statement :  has-value: `(a)↓` uimplies: `b 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: `b 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