---

Step * of Lemma member-sub-mset

∀[T:Type]. ∀L1,L2:T List.  (sub-mset(T; L1; L2) ⇒ (∀x:T. ((x ∈ L1) ⇒ (x ∈ L2))))
BY
{ (Auto THEN (FLemma `sub-mset-contains` [-3] THENA Auto)) }

1
1. [T] : Type
2. L1 : T List@i
3. L2 : T List@i
4. sub-mset(T; L1; L2)@i
5. x : T@i
6. (x ∈ L1)@i
7. L1 ⊆ L2
⊢ (x ∈ L2)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.    (sub-mset(T;  L1;  L2)  {}\mRightarrow{}  (\mforall{}x:T.  ((x  \mmember{}  L1)  {}\mRightarrow{}  (x  \mmember{}  L2))))


By

---

Latex:
(Auto  THEN  (FLemma  `sub-mset-contains`  [-3]  THENA  Auto))

---

Home Index