---

Step * of Lemma function-not-int

∀[A:Type]. ∀[B:A ⟶ Type].  ∀[f:a:A ⟶ B[a]]. (isint(f) ~ ff) supposing ↓∃a:A. value-type(B[a])
BY
{ TACTIC:(Auto THEN ExRepD THEN (Assert (f a)↓ BY Auto) THEN HasValueD (-1) THEN (Assert ¬(⊥)↓ BY Auto)) }

1
1. A : Type
2. B : A ⟶ Type
3. a : A
4. value-type(B[a])
5. f : a:A ⟶ B[a]
6. (f a)↓
7. (f)↓
8. ¬(⊥)↓
⊢ isint(f) = ff

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    \mforall{}[f:a:A  {}\mrightarrow{}  B[a]].  (isint(f)  \msim{}  ff)  supposing  \mdownarrow{}\mexists{}a:A.  value-type(B[a])


By

---

Latex:
TACTIC:(Auto
                THEN  ExRepD
                THEN  (Assert  (f  a)\mdownarrow{}  BY
                                        Auto)
                THEN  HasValueD  (-1)
                THEN  (Assert  \mneg{}(\mbot{})\mdownarrow{}  BY
                                        Auto))

---

Home Index