---

Step * of Lemma permutation-strong-subtype

∀[A,B:Type].
  ∀L1:B List. ∀L2:A List.  (permutation(A;L1;L2) ⇒ {(L2 ∈ B List) ∧ permutation(B;L1;L2)}) 
  supposing strong-subtype(B;A)
BY
{ (Auto THEN (FLemma `member-permutation` [-1] THENA Auto) THEN Assert ⌜L2 ∈ B List⌝⋅) }

1
.....assertion..... 
1. [A] : Type
2. [B] : Type
3. strong-subtype(B;A)
4. L1 : B List
5. L2 : A List
6. permutation(A;L1;L2)
7. ∀a:A. ((a ∈ L1) ⇐⇒ (a ∈ L2))
⊢ L2 ∈ B List

2
1. [A] : Type
2. [B] : Type
3. strong-subtype(B;A)
4. L1 : B List
5. L2 : A List
6. permutation(A;L1;L2)
7. ∀a:A. ((a ∈ L1) ⇐⇒ (a ∈ L2))
8. L2 ∈ B List
⊢ {(L2 ∈ B List) ∧ permutation(B;L1;L2)}

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}L1:B  List.  \mforall{}L2:A  List.    (permutation(A;L1;L2)  {}\mRightarrow{}  \{(L2  \mmember{}  B  List)  \mwedge{}  permutation(B;L1;L2)\}) 
    supposing  strong-subtype(B;A)


By

---

Latex:
(Auto  THEN  (FLemma  `member-permutation`  [-1]  THENA  Auto)  THEN  Assert  \mkleeneopen{}L2  \mmember{}  B  List\mkleeneclose{}\mcdot{})

---

Home Index