Nuprl Lemma : uall-union

[A,B:Type].  ∀P:(A B) ⟶ ℙ((∀[x:A B]. P[x])  ((∀[a:A]. P[inl a]) ∧ (∀[b:B]. P[inr ])))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q and: P ∧ Q function: x:A ⟶ B[x] inr: inr  inl: inl x union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q cand: c∧ B member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] guard: {T}
Lemmas referenced :  uall_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut hypothesisEquality independent_pairFormation hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin unionEquality sqequalRule lambdaEquality applyEquality functionEquality cumulativity universeEquality inlEquality inrEquality

Latex:
\mforall{}[A,B:Type].    \mforall{}P:(A  +  B)  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}[x:A  +  B].  P[x])  {}\mRightarrow{}  ((\mforall{}[a:A].  P[inl  a])  \mwedge{}  (\mforall{}[b:B].  P[inr  b  ])))



Date html generated: 2016_05_15-PM-03_24_45
Last ObjectModification: 2015_12_27-PM-01_06_11

Theory : general


Home Index