---

Step * of Lemma Rice-theorem-for-Type

∀F:Type ⟶ 𝔹. ((∀X,Y:Type.  (X ~ Y ⇒ F X = F Y)) ⇒ ((F = (λT.tt) ∈ (Type ⟶ 𝔹)) ∨ (F = (λT.ff) ∈ (Type ⟶ 𝔹))))
BY
{ (Auto THEN Assert ⌜∀X,Y:Type.  F X = F Y⌝⋅) }

1
.....assertion..... 
1. F : Type ⟶ 𝔹
2. ∀X,Y:Type.  (X ~ Y ⇒ F X = F Y)
⊢ ∀X,Y:Type.  F X = F Y

2
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 ⟶ 𝔹))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}X,Y:Type.    F  X  =  F  Y\mkleeneclose{}\mcdot{})

---

Home Index