---

Step * of Lemma l_all_functionality_wrt_permutation

∀[A:Type]. ∀P:A ⟶ ℙ. ∀L1,L2:A List.  (permutation(A;L1;L2) ⇒ {(∀x∈L1.P[x]) ⇐⇒ (∀x∈L2.P[x])})
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (All (RWO "l_all_iff") THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN FLemma `member-permutation` [5]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}P:A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}L1,L2:A  List.    (permutation(A;L1;L2)  {}\mRightarrow{}  \{(\mforall{}x\mmember{}L1.P[x])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x\mmember{}L2.P[x])\})


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (All  (RWO  "l\_all\_iff")  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  FLemma  `member-permutation`  [5]
  THEN  Auto)

---

Home Index