---

Step * of Lemma strong-subtype-eq2

∀[A,B:Type]. ∀[b:B]. ∀[a:A].  (b = a ∈ A) supposing ((b = a ∈ B) and strong-subtype(A;B))
BY
{ ((InstLemma `strong-subtype-eq1` [])
   THEN ((RepeatFor 5 (((ParallelOp (-1)) THENA (Auto THEN DoSubsume THEN Auto)))
          THEN (D 0 THENA (Auto THEN DoSubsume THEN Auto))
          ))⋅
   ) }

1
1. ∀[A,B:Type]. ∀[b:B]. ∀[a:A].  ((b ∈ A) c∧ (b = a ∈ A)) supposing ((b = a ∈ B) and strong-subtype(A;B))
2. A : Type
3. ∀[B:Type]. ∀[b:B]. ∀[a:A].  ((b ∈ A) c∧ (b = a ∈ A)) supposing ((b = a ∈ B) and strong-subtype(A;B))
4. B : Type
5. ∀[b:B]. ∀[a:A].  ((b ∈ A) c∧ (b = a ∈ A)) supposing ((b = a ∈ B) and strong-subtype(A;B))
6. b : B
7. ∀[a:A]. ((b ∈ A) c∧ (b = a ∈ A)) supposing ((b = a ∈ B) and strong-subtype(A;B))
8. a : A
9. strong-subtype(A;B)
10. (b ∈ A) c∧ (b = a ∈ A) supposing b = a ∈ B
11. b = a ∈ B
⊢ b = a ∈ A

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[b:B].  \mforall{}[a:A].    (b  =  a)  supposing  ((b  =  a)  and  strong-subtype(A;B))


By

---

Latex:
((InstLemma  `strong-subtype-eq1`  [])
  THEN  ((RepeatFor  5  (((ParallelOp  (-1))  THENA  (Auto  THEN  DoSubsume  THEN  Auto)))
                THEN  (D  0  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
                ))\mcdot{}
  )

---

Home Index