### Nuprl Lemma : comb_for_ifthenelse_wf

`λb,A,p,q,z. if b then p else q fi  ∈ b:𝔹 ⟶ A:Type ⟶ p:A ⟶ q:A ⟶ (↓True) ⟶ A`

Proof

Definitions occuring in Statement :  ifthenelse: `if b then t else f fi ` bool: `𝔹` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ`
Lemmas referenced :  ifthenelse_wf squash_wf true_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut introduction extract_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality

Latex:
\mlambda{}b,A,p,q,z.  if  b  then  p  else  q  fi    \mmember{}  b:\mBbbB{}  {}\mrightarrow{}  A:Type  {}\mrightarrow{}  p:A  {}\mrightarrow{}  q:A  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  A

Date html generated: 2018_05_21-PM-06_20_14
Last ObjectModification: 2018_05_19-PM-05_32_21

Theory : list!

Home Index