---

Step * 2 1 of Lemma split_tail_trivial

.....antecedent..... 
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀b:A. ((b ∈ [u / v]) ⇒ (↑f[b]))
⊢ ∀b:A. ((b ∈ v) ⇒ (↑f[b]))
BY
{ (RepeatFor 2 (ParallelOp (-1)) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  \mforall{}b:A.  ((b  \mmember{}  [u  /  v])  {}\mRightarrow{}  (\muparrow{}f[b]))
\mvdash{}  \mforall{}b:A.  ((b  \mmember{}  v)  {}\mRightarrow{}  (\muparrow{}f[b]))


By

---

Latex:
(RepeatFor  2  (ParallelOp  (-1))  THEN  Auto)

---

Home Index