---

Step * 2 1 of Lemma first-member-cons

.....truecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. x = u ∈ T
7. ↑(P u)
⊢ first-member(T;x;[u / L];P)
BY
{ (With ⌜0⌝ (D 0)⋅ THEN Reduce 0 THEN Auto THEN Auto')⋅ }

---

Latex:

---

Latex:
.....truecase..... 
1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  u  :  T
5.  L  :  T  List
6.  x  =  u
7.  \muparrow{}(P  u)
\mvdash{}  first-member(T;x;[u  /  L];P)


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto  THEN  Auto')\mcdot{}

---

Home Index