---

Step * of Lemma set-equal-permute

∀[T:Type]. ∀as,bs:T List.  set-equal(T;as @ bs;bs @ as)
BY
{ (Auto THEN Unfold `set-equal` 0 THEN RWO "member_append" 0  THEN Auto THEN ProveProp THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}as,bs:T  List.    set-equal(T;as  @  bs;bs  @  as)


By

---

Latex:
(Auto  THEN  Unfold  `set-equal`  0  THEN  RWO  "member\_append"  0    THEN  Auto  THEN  ProveProp  THEN  Auto)

---

Home Index