Nuprl Lemma : fun_thru_ite

[S,T:Type]. ∀[f:S ⟶ T]. ∀[b:𝔹]. ∀[p,q:S].  ((f if then else fi if then else fi  ∈ T)


Proof




Definitions occuring in Statement :  ifthenelse: if then else fi  bool: 𝔹 uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False
Lemmas referenced :  bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut hypothesisEquality thin extract_by_obid hypothesis lambdaFormation sqequalHypSubstitution unionElimination equalityElimination isectElimination because_Cache productElimination independent_isectElimination sqequalRule applyEquality dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination voidElimination Error :inhabitedIsType,  isect_memberEquality axiomEquality Error :universeIsType,  Error :functionIsType,  functionEquality universeEquality

Latex:
\mforall{}[S,T:Type].  \mforall{}[f:S  {}\mrightarrow{}  T].  \mforall{}[b:\mBbbB{}].  \mforall{}[p,q:S].
    ((f  if  b  then  p  else  q  fi  )  =  if  b  then  f  p  else  f  q  fi  )



Date html generated: 2019_06_20-AM-11_31_43
Last ObjectModification: 2018_09_26-AM-11_28_10

Theory : bool_1


Home Index