---

Step * of Lemma ball_functionality_wrt_bimplies

∀T:Type. ∀as:T List. ∀P,Q:T ⟶ 𝔹.  ((∀x:T. (↑(P[x] ⇒b Q[x]))) ⇒ (↑(∀bx(:T) ∈ as. P[x] ⇒b (∀bx(:T) ∈ as. Q[x]))))
BY
{ (RepeatFor 5 (Intro)
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN (Unfold `bimplies` 0 THEN ListInd 2)
   THEN Reduce 0
   THEN Try (Trivial)) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. Q : T ⟶ 𝔹
4. ∀x:T. ↑Q[x] supposing ↑P[x]
5. u : T
6. v : T List
7. ↑((¬b(∀bx(:T) ∈ v. P[x])) ∨b(∀bx(:T) ∈ v. Q[x]))
⊢ ↑((¬b(P[u] ∧b (∀bx(:T) ∈ v. P[x]))) ∨b(Q[u] ∧b (∀bx(:T) ∈ v. Q[x])))

---

Latex:

---

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


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  (Unfold  `bimplies`  0  THEN  ListInd  2)
  THEN  Reduce  0
  THEN  Try  (Trivial))

---

Home Index