---

Step * of Lemma bottom-pair-member-approx-type

∀[A,B:Type].  (A ⇒ B ⇒ (<⊥, ⊥> ∈ approx-type(A × B)))
BY
{ (Auto
   THEN (RenameVar `a' (-2) THEN (PointwiseFunctionalityForEquality (-2) THENW Auto))
   THEN RenameVar `b' (-1)
   THEN (PointwiseFunctionalityForEquality (-1) THENW Auto)
   THEN Fold `member` 0) }

1
1. A : Type
2. B : Type
3. a : Base
4. a1 : Base
5. a = a1 ∈ A
6. b : Base
7. b1 : Base
8. b = b1 ∈ B
⊢ <⊥, ⊥> ∈ approx-type(A × B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (A  {}\mRightarrow{}  B  {}\mRightarrow{}  (<\mbot{},  \mbot{}>  \mmember{}  approx-type(A  \mtimes{}  B)))


By

---

Latex:
(Auto
  THEN  (RenameVar  `a'  (-2)  THEN  (PointwiseFunctionalityForEquality  (-2)  THENW  Auto))
  THEN  RenameVar  `b'  (-1)
  THEN  (PointwiseFunctionalityForEquality  (-1)  THENW  Auto)
  THEN  Fold  `member`  0)

---

Home Index