---

Step * 1 1 of Lemma cons_functionality_wrt_permr


1. T : Type
2. a : T
3. b : T
4. as : T List
5. bs : T List
6. a = b ∈ T
7. ||as|| = ||bs|| ∈ ℤ
8. p : Sym(||as||)
9. ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T)
10. (||as|| + 1) = (||bs|| + 1) ∈ ℤ
⊢ ∃p:Sym(||as|| + 1). ∀i:ℕ||as|| + 1. ([a / as][p.f i] = [b / bs][i] ∈ T)
BY
{ (% extend_perm extends the hi end, we need the lo end
   extended here%
   
   With conj{↔p{||as|| + 1}}(↑{||as||}(conj{↔p{||as||}}(p))) (D 0)
   THENA Auto
   ) }

1
1. T : Type
2. a : T
3. b : T
4. as : T List
5. bs : T List
6. a = b ∈ T
7. ||as|| = ||bs|| ∈ ℤ
8. p : Sym(||as||)
9. ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T)
10. (||as|| + 1) = (||bs|| + 1) ∈ ℤ
⊢ ∀i:ℕ||as|| + 1. ([a / as][conj{↔p{||as|| + 1}}(↑{||as||}(conj{↔p{||as||}}(p))).f i] = [b / bs][i] ∈ T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  T
3.  b  :  T
4.  as  :  T  List
5.  bs  :  T  List
6.  a  =  b
7.  ||as||  =  ||bs||
8.  p  :  Sym(||as||)
9.  \mforall{}i:\mBbbN{}||as||.  (as[p.f  i]  =  bs[i])
10.  (||as||  +  1)  =  (||bs||  +  1)
\mvdash{}  \mexists{}p:Sym(||as||  +  1).  \mforall{}i:\mBbbN{}||as||  +  1.  ([a  /  as][p.f  i]  =  [b  /  bs][i])


By

---

Latex:
(\%  extend\_perm  extends  the  hi  end,  we  need  the  lo  end
  extended  here\%
 
  With  conj\{\mrightleftharpoons{}p\{||as||  +  1\}\}(\muparrow{}\{||as||\}(conj\{\mrightleftharpoons{}p\{||as||\}\}(p)))  (D  0)
  THENA  Auto
  )

---

Home Index