---

Step * 2 of Lemma Rice-theorem-for-Type


1. F : Type ⟶ 𝔹
2. ∀X,Y:Type.  (X ~ Y ⇒ F X = F Y)
3. ∀X,Y:Type.  F X = F Y
⊢ (F = (λT.tt) ∈ (Type ⟶ 𝔹)) ∨ (F = (λT.ff) ∈ (Type ⟶ 𝔹))
BY
{ ((D -1 With ⌜Void⌝  THENA Auto) THEN MoveToConcl (-1) THEN BoolCase ⌜F Void⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}X,Y:Type.    (X  \msim{}  Y  {}\mRightarrow{}  F  X  =  F  Y)
3.  \mforall{}X,Y:Type.    F  X  =  F  Y
\mvdash{}  (F  =  (\mlambda{}T.tt))  \mvee{}  (F  =  (\mlambda{}T.ff))


By

---

Latex:
((D  -1  With  \mkleeneopen{}Void\mkleeneclose{}    THENA  Auto)  THEN  MoveToConcl  (-1)  THEN  BoolCase  \mkleeneopen{}F  Void\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index