---

Step * of Lemma ball_functionality_wrt_permr

∀T:Type. ∀as,bs:T List. ∀P,Q:T ⟶ 𝔹.  ((as ≡(T) bs) ⇒ (∀x:T. P[x] = Q[x]) ⇒ ∀bx(:T) ∈ as. P[x] = ∀bx(:T) ∈ bs. Q[x])
BY
{ ((RepD THENM Unfold `ball` 0) THENA Auto) }

1
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]

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as,bs:T  List.  \mforall{}P,Q:T  {}\mrightarrow{}  \mBbbB{}.
    ((as  \mequiv{}(T)  bs)  {}\mRightarrow{}  (\mforall{}x:T.  P[x]  =  Q[x])  {}\mRightarrow{}  \mforall{}\msubb{}x(:T)  \mmember{}  as.  P[x]  =  \mforall{}\msubb{}x(:T)  \mmember{}  bs.  Q[x])


By

---

Latex:
((RepD  THENM  Unfold  `ball`  0)  THENA  Auto)

---

Home Index