Nuprl Lemma : eq_int_cases_test
∀[A:Type]. ∀x,y:A. ∀[P:A ⟶ ℙ]. ∀i,j:ℤ. ((P if (i =z j) then x else y fi ) ⇒ (P if (i =z j) then x else y fi ))
Proof
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ
Lemmas referenced :
ifthenelse_wf,
eq_int_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
lambdaFormation,
hypothesis,
applyEquality,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
intEquality,
Error :functionIsType,
Error :inhabitedIsType,
Error :universeIsType,
universeEquality
Latex:
\mforall{}[A:Type]
\mforall{}x,y:A.
\mforall{}[P:A {}\mrightarrow{} \mBbbP{}]. \mforall{}i,j:\mBbbZ{}. ((P if (i =\msubz{} j) then x else y fi ) {}\mRightarrow{} (P if (i =\msubz{} j) then x else y fi ))
Date html generated:
2019_06_20-AM-11_32_04
Last ObjectModification:
2018_09_26-AM-11_28_11
Theory : bool_1
Home
Index