---

Step * 1 of Lemma safety_nil


1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. l : T List
4. P[l]
5. ∀tr1,tr2:T List.  (tr1 ≤ tr2 ⇒ P[tr2] ⇒ P[tr1])
⊢ P[[]]
BY
{ (BackThruHyp'' (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  l  :  T  List
4.  P[l]
5.  \mforall{}tr1,tr2:T  List.    (tr1  \mleq{}  tr2  {}\mRightarrow{}  P[tr2]  {}\mRightarrow{}  P[tr1])
\mvdash{}  P[[]]


By

---

Latex:
(BackThruHyp''  (-1)  THEN  Auto)

---

Home Index