---

Step * 1 1 1 of Lemma can-find-first


1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∃x:T [first-member(T;x;v;P)]
⊢ ∃x:T [first-member(T;x;[u / v];P)]
BY
{ xxx(RenameVar `z' (-1)
      THEN D -1
      THEN UseWitness ⌜if P u then u else z fi ⌝⋅
      THEN MemTypeCD
      THEN Auto
      THEN AutoSplit
      THEN RWO "first-member-cons" 0
      THEN Auto
      THEN AutoSplit)xxx }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mexists{}x:T  [first-member(T;x;v;P)]
\mvdash{}  \mexists{}x:T  [first-member(T;x;[u  /  v];P)]


By

---

Latex:
xxx(RenameVar  `z'  (-1)
        THEN  D  -1
        THEN  UseWitness  \mkleeneopen{}if  P  u  then  u  else  z  fi  \mkleeneclose{}\mcdot{}
        THEN  MemTypeCD
        THEN  Auto
        THEN  AutoSplit
        THEN  RWO  "first-member-cons"  0
        THEN  Auto
        THEN  AutoSplit)xxx

---

Home Index