---

Step * 1 of Lemma fset-pair-symmetry

.....antecedent..... 
1. T : Type
2. a : T
3. b : T
⊢ set-equal(T;[a; b];[b; a])
BY
{ ((D 0 THENA Auto) THEN (RWW "cons_member nil_member" 0 THEN Auto) THEN SplitOrHyps THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  a  :  T
3.  b  :  T
\mvdash{}  set-equal(T;[a;  b];[b;  a])


By

---

Latex:
((D  0  THENA  Auto)  THEN  (RWW  "cons\_member  nil\_member"  0  THEN  Auto)  THEN  SplitOrHyps  THEN  Auto)

---

Home Index