---

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

.....assertion..... 
1. F : Type ⟶ 𝔹
2. ∀X,Y:Type.  (X ~ Y ⇒ F X = F Y)
⊢ ∀X,Y:Type.  F X = F Y
BY
{ (Auto THEN (BoolCase ⌜F X⌝⋅ THENA Auto) THEN BoolCase ⌜F Y⌝⋅ THEN Auto) }

1
1. F : Type ⟶ 𝔹
2. ∀X,Y:Type.  (X ~ Y ⇒ F X = F Y)
3. X : Type
4. Y : Type
5. ¬↑(F Y)
6. ↑(F X)
⊢ tt = ff

2
1. F : Type ⟶ 𝔹
2. ∀X,Y:Type.  (X ~ Y ⇒ F X = F Y)
3. X : Type
4. ¬↑(F X)
5. Y : Type
6. ↑(F Y)
⊢ ff = tt

---

Latex:

---

Latex:
.....assertion..... 
1.  F  :  Type  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}X,Y:Type.    (X  \msim{}  Y  {}\mRightarrow{}  F  X  =  F  Y)
\mvdash{}  \mforall{}X,Y:Type.    F  X  =  F  Y


By

---

Latex:
(Auto  THEN  (BoolCase  \mkleeneopen{}F  X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  BoolCase  \mkleeneopen{}F  Y\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index