Nuprl Lemma : ifthenelse_wf

[b:𝔹]. ∀[A:Type]. ∀[p,q:A].  (if then else fi  ∈ A)


Proof




Definitions occuring in Statement :  ifthenelse: if then else fi  bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] ifthenelse: if then else fi  bool: 𝔹
Lemmas referenced :  bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity hypothesisEquality because_Cache universeEquality cut lemma_by_obid hypothesis isect_memberFormation introduction sqequalHypSubstitution sqequalRule axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality isectElimination thin unionElimination

Latex:
\mforall{}[b:\mBbbB{}].  \mforall{}[A:Type].  \mforall{}[p,q:A].    (if  b  then  p  else  q  fi    \mmember{}  A)



Date html generated: 2016_05_13-PM-03_20_17
Last ObjectModification: 2015_12_26-AM-09_10_56

Theory : union


Home Index