Nuprl Lemma : only-two-bools
∀f:⋂T:Type. (T ⟶ T ⟶ T). ((f = (λx,y. x) ∈ (⋂T:Type. (T ⟶ T ⟶ T))) ∨ (f = (λx,y. y) ∈ (⋂T:Type. (T ⟶ T ⟶ T))))
Proof
Definitions occuring in Statement :
all: ∀x:A. B[x],
or: P ∨ Q,
lambda: λx.A[x],
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas referenced :
polymorphic-choice
Rules used in proof :
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}f:\mcap{}T:Type. (T {}\mrightarrow{} T {}\mrightarrow{} T). ((f = (\mlambda{}x,y. x)) \mvee{} (f = (\mlambda{}x,y. y)))
Date html generated:
2019_10_15-AM-11_14_34
Last ObjectModification:
2019_06_12-AM-09_24_42
Theory : general
Home
Index