---

Step * 1 of Lemma ball_functionality_wrt_permr


1. T : Type
2. as : T List
3. bs : T List
4. P : T ⟶ 𝔹
5. Q : T ⟶ 𝔹
6. as ≡(T) bs
7. ∀x:T. P[x] = Q[x]
⊢ For{<𝔹,∧b>} x ∈ as. P[x] = For{<𝔹,∧b>} x ∈ bs. Q[x]
BY
{ (RewriteWith [6; 7] [] 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  P  :  T  {}\mrightarrow{}  \mBbbB{}
5.  Q  :  T  {}\mrightarrow{}  \mBbbB{}
6.  as  \mequiv{}(T)  bs
7.  \mforall{}x:T.  P[x]  =  Q[x]
\mvdash{}  For\{<\mBbbB{},\mwedge{}\msubb{}>\}  x  \mmember{}  as.  P[x]  =  For\{<\mBbbB{},\mwedge{}\msubb{}>\}  x  \mmember{}  bs.  Q[x]


By

---

Latex:
(RewriteWith  [6;  7]  []  0  THEN  Auto)

---

Home Index