---

Step * 1 of Lemma fset-union_wf

.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
6. x ∈ T List
7. x1 ∈ T List
8. set-equal(T;x;x1)
9. y : Base
10. y1 : Base
11. y = y1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
12. y ∈ T List
13. y1 ∈ T List
14. set-equal(T;y;y1)
⊢ set-equal(T;x ⋃ y;x1 ⋃ y1)
BY
{ ((D 0 THENA Auto) THEN (RWO "member-union" 0 THEN Auto) THEN ParallelLast THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  Base
4.  x1  :  Base
5.  x  =  x1
6.  x  \mmember{}  T  List
7.  x1  \mmember{}  T  List
8.  set-equal(T;x;x1)
9.  y  :  Base
10.  y1  :  Base
11.  y  =  y1
12.  y  \mmember{}  T  List
13.  y1  \mmember{}  T  List
14.  set-equal(T;y;y1)
\mvdash{}  set-equal(T;x  \mcup{}  y;x1  \mcup{}  y1)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (RWO  "member-union"  0  THEN  Auto)  THEN  ParallelLast  THEN  Auto)\mcdot{}

---

Home Index