---

Step * 1 of Lemma list-eq-subtype


1. A : Type
2. d1 : A List
3. d2 : A List
4. d1 = d2 ∈ (A List)
⊢ d1 = d2 ∈ ({a:A| (a ∈ d1)}  List)
BY
{ (InstLemma `list-eq-subtype1` [⌜A⌝;⌜λx.(x ∈ d1)⌝;⌜d1⌝;⌜d2⌝]⋅
   THENA (Auto THEN RepUR ``so_apply`` 0 THEN Try (Complete ((BLemma `list-subtype` THEN Auto))))
   ) }

1
1. A : Type
2. d1 : A List
3. d2 : A List
4. d1 = d2 ∈ (A List)
⊢ d2 ∈ {a:A| (a ∈ d1)}  List

2
1. A : Type
2. d1 : A List
3. d2 : A List
4. d1 = d2 ∈ (A List)
5. d1 = d2 ∈ ({a:A| λx.(x ∈ d1)[a]}  List)
⊢ d1 = d2 ∈ ({a:A| (a ∈ d1)}  List)

---

Latex:

---

Latex:

1.  A  :  Type
2.  d1  :  A  List
3.  d2  :  A  List
4.  d1  =  d2
\mvdash{}  d1  =  d2


By

---

Latex:
(InstLemma  `list-eq-subtype1`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(x  \mmember{}  d1)\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  RepUR  ``so\_apply``  0  THEN  Try  (Complete  ((BLemma  `list-subtype`  THEN  Auto))))
  )

---

Home Index