---

Step * 1 of Lemma subtype-approx-type

.....subterm..... T:t
1:n
1. T : Type
2. mono(T) ∨ (T ⊆r Base)
3. x : T
⊢ x ∈ approx-type(T)
BY
{ ((PointwiseFunctionalityForEquality (-1) THENW Auto)
   THEN PerEqCD
   THEN Try (Fold `approx-type` 0)
   THEN Auto
   THEN RepUR ``so_lambda`` 0
   THEN RenameVar `y' (-2)) }

1
1. T : Type
2. mono(T) ∨ (T ⊆r Base)
3. x : Base
4. y : Base
5. x = y ∈ T
⊢ approx-per(T;x;y)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  T  :  Type
2.  mono(T)  \mvee{}  (T  \msubseteq{}r  Base)
3.  x  :  T
\mvdash{}  x  \mmember{}  approx-type(T)


By

---

Latex:
((PointwiseFunctionalityForEquality  (-1)  THENW  Auto)
  THEN  PerEqCD
  THEN  Try  (Fold  `approx-type`  0)
  THEN  Auto
  THEN  RepUR  ``so\_lambda``  0
  THEN  RenameVar  `y'  (-2))

---

Home Index