---

Step * 2 of Lemma free-vs-subtype


1. S : Type
2. T : Type
3. S ⊆r T
4. K : CRng
5. basic-formal-sum(K;S) ⊆r basic-formal-sum(K;T)
6. x : Base
7. x1 : Base
8. x = x1 ∈ (a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b))
9. x ∈ basic-formal-sum(K;S)
10. x1 ∈ basic-formal-sum(K;S)
11. bfs-equiv(K;S;x;x1)
⊢ EquivRel(basic-formal-sum(K;S);x,y.bfs-equiv(K;T;x;y))
BY
{ ((Assert EquivRel(basic-formal-sum(K;T);x,y.bfs-equiv(K;T;x;y)) BY Auto) THEN RepeatFor 8 (ParallelLast)) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  T  :  Type
3.  S  \msubseteq{}r  T
4.  K  :  CRng
5.  basic-formal-sum(K;S)  \msubseteq{}r  basic-formal-sum(K;T)
6.  x  :  Base
7.  x1  :  Base
8.  x  =  x1
9.  x  \mmember{}  basic-formal-sum(K;S)
10.  x1  \mmember{}  basic-formal-sum(K;S)
11.  bfs-equiv(K;S;x;x1)
\mvdash{}  EquivRel(basic-formal-sum(K;S);x,y.bfs-equiv(K;T;x;y))


By

---

Latex:
((Assert  EquivRel(basic-formal-sum(K;T);x,y.bfs-equiv(K;T;x;y))  BY
                Auto)
  THEN  RepeatFor  8  (ParallelLast)
  )

---

Home Index