---

Step * 1 of Lemma strong-subtype-eq2


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
BY
{ ((D (-2)) THEN Try (Trivial) THEN (D (-1)) THEN Trivial)⋅ }

---

Latex:

---

Latex:

1.  \mforall{}[A,B:Type].  \mforall{}[b:B].  \mforall{}[a:A].    ((b  \mmember{}  A)  c\mwedge{}  (b  =  a))  supposing  ((b  =  a)  and  strong-subtype(A;B))
2.  A  :  Type
3.  \mforall{}[B:Type].  \mforall{}[b:B].  \mforall{}[a:A].    ((b  \mmember{}  A)  c\mwedge{}  (b  =  a))  supposing  ((b  =  a)  and  strong-subtype(A;B))
4.  B  :  Type
5.  \mforall{}[b:B].  \mforall{}[a:A].    ((b  \mmember{}  A)  c\mwedge{}  (b  =  a))  supposing  ((b  =  a)  and  strong-subtype(A;B))
6.  b  :  B
7.  \mforall{}[a:A].  ((b  \mmember{}  A)  c\mwedge{}  (b  =  a))  supposing  ((b  =  a)  and  strong-subtype(A;B))
8.  a  :  A
9.  strong-subtype(A;B)
10.  (b  \mmember{}  A)  c\mwedge{}  (b  =  a)  supposing  b  =  a
11.  b  =  a
\mvdash{}  b  =  a


By

---

Latex:
((D  (-2))  THEN  Try  (Trivial)  THEN  (D  (-1))  THEN  Trivial)\mcdot{}

---

Home Index