---

Step * of Lemma member-rev-append

No Annotations
∀[T:Type]. ∀x:T. ∀as,bs:T List.  ((x ∈ rev(as) + bs) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))
BY
{ (Intros
   THEN (RWO "rev-append-property" 0 THENA Auto)
   THEN Fold `reverse` 0
   THEN RWW "member_append member-reverse" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}as,bs:T  List.    ((x  \mmember{}  rev(as)  +  bs)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  as)  \mvee{}  (x  \mmember{}  bs))


By

---

Latex:
(Intros
  THEN  (RWO  "rev-append-property"  0  THENA  Auto)
  THEN  Fold  `reverse`  0
  THEN  RWW  "member\_append  member-reverse"  0
  THEN  Auto)

---

Home Index