Nuprl Lemma : decide_wf

[T1,T2,T3:Type]. ∀[x:T1 T2]. ∀[l:T1 ⟶ T3]. ∀[r:T2 ⟶ T3].  (case of inl(a) => l[a] inr(b) => r[b] ∈ T3)


Definitions occuring in Statement :  uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] decide: case of inl(x) => s[x] inr(y) => t[y] union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q so_apply: x[s] prop:
Lemmas referenced :  equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality equalityTransitivity hypothesis equalitySymmetry thin unionEquality lambdaFormation unionElimination sqequalRule applyEquality extract_by_obid sqequalHypSubstitution isectElimination dependent_functionElimination independent_functionElimination axiomEquality functionEquality isect_memberEquality because_Cache universeEquality

\mforall{}[T1,T2,T3:Type].  \mforall{}[x:T1  +  T2].  \mforall{}[l:T1  {}\mrightarrow{}  T3].  \mforall{}[r:T2  {}\mrightarrow{}  T3].
    (case  x  of  inl(a)  =>  l[a]  |  inr(b)  =>  r[b]  \mmember{}  T3)

Date html generated: 2019_10_15-AM-11_06_47
Last ObjectModification: 2018_08_21-PM-01_58_34

Theory : general

Home Index