Nuprl Lemma : member-ite
∀b:𝔹. ∀[T:Type]. ∀A,B:T List. ∀x:T. ((x ∈ if b then A else B fi ) ⇐⇒ ((↑b) ∧ (x ∈ A)) ∨ ((¬↑b) ∧ (x ∈ B)))
Proof
Definitions occuring in Statement :
l_member: (x ∈ l),
list: T List,
assert: ↑b,
ifthenelse: if b then t else f fi ,
bool: 𝔹,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
universe: Type
Lemmas :
bool_wf,
eqtt_to_assert,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot
\mforall{}b:\mBbbB{}
\mforall{}[T:Type]
\mforall{}A,B:T List. \mforall{}x:T. ((x \mmember{} if b then A else B fi ) \mLeftarrow{}{}\mRightarrow{} ((\muparrow{}b) \mwedge{} (x \mmember{} A)) \mvee{} ((\mneg{}\muparrow{}b) \mwedge{} (x \mmember{} B)))
Date html generated:
2015_07_17-AM-09_04_57
Last ObjectModification:
2015_01_27-PM-00_53_21
Home
Index