---

Step * 1 of Lemma strong-subtype-fset-member-type


1. A : Type
2. B : Type
3. eq : EqDecider(B)
4. strong-subtype(A;B)
5. s : fset(A)
6. x : B
7. s ∈ fset(B)
8. x ∈ s
⊢ x ∈ A
BY
{ (newQuotD 5⋅
   THEN TACTIC:Thin (-2)
   THEN Unfold `fset-member` -1
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN FLemma `strong-subtype-l_member-type` [4;-1]⋅⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  eq  :  EqDecider(B)
4.  strong-subtype(A;B)
5.  s  :  fset(A)
6.  x  :  B
7.  s  \mmember{}  fset(B)
8.  x  \mmember{}  s
\mvdash{}  x  \mmember{}  A


By

---

Latex:
(newQuotD  5\mcdot{}
  THEN  TACTIC:Thin  (-2)
  THEN  Unfold  `fset-member`  -1
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  FLemma  `strong-subtype-l\_member-type`  [4;-1]\mcdot{}\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index