---

Step * 1 of Lemma cons-wf-fset

.....antecedent..... 
1. T : Type
2. s : Base
3. s1 : Base
4. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
5. s ∈ T List
6. s1 ∈ T List
7. set-equal(T;s;s1)
8. x : T
⊢ set-equal(T;[x / s];[x / s1])
BY
{ (RepeatFor 2 (ParallelOp -2) THEN RWW "cons_member -1" 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  s  :  Base
3.  s1  :  Base
4.  s  =  s1
5.  s  \mmember{}  T  List
6.  s1  \mmember{}  T  List
7.  set-equal(T;s;s1)
8.  x  :  T
\mvdash{}  set-equal(T;[x  /  s];[x  /  s1])


By

---

Latex:
(RepeatFor  2  (ParallelOp  -2)  THEN  RWW  "cons\_member  -1"  0  THEN  Auto)

---

Home Index