---

Step * 1 1 of Lemma permutation-cons

.....assertion..... 
1. [A] : Type
2. x : A
3. L1 : A List
4. L2 : A List
5. permutation(A;[x / L1];L2)
⊢ ∃as,bs:A List. (L2 = (as @ [x / bs]) ∈ (A List))
BY
{ ((Assert (x ∈ L2) BY
          ((FLemma `permutation_inversion` [-1] THENA Auto)
           THEN (FLemma `permutation-contains` [-1] THENA Auto)
           THEN Unfold `l_contains` (-1)
           THEN With ⌜0⌝ (D (-1)) ⋅
           THEN All Reduce
           THEN Auto')⋅)
   THEN Try ((RWO "l_member_decomp" (-1) THEN Auto))
   ) }

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  Type
2.  x  :  A
3.  L1  :  A  List
4.  L2  :  A  List
5.  permutation(A;[x  /  L1];L2)
\mvdash{}  \mexists{}as,bs:A  List.  (L2  =  (as  @  [x  /  bs]))


By

---

Latex:
((Assert  (x  \mmember{}  L2)  BY
                ((FLemma  `permutation\_inversion`  [-1]  THENA  Auto)
                  THEN  (FLemma  `permutation-contains`  [-1]  THENA  Auto)
                  THEN  Unfold  `l\_contains`  (-1)
                  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))  \mcdot{}
                  THEN  All  Reduce
                  THEN  Auto')\mcdot{})
  THEN  Try  ((RWO  "l\_member\_decomp"  (-1)  THEN  Auto))
  )

---

Home Index