---

Step * of Lemma safety_nil

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].  ((∃l:T List. P[l]) ⇒ safety(T;x.P[x]) ⇒ P[[]])
BY
{ ((Unfold `safety` 0 THEN Auto) THEN ExRepD) }

1
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[[]]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].    ((\mexists{}l:T  List.  P[l])  {}\mRightarrow{}  safety(T;x.P[x])  {}\mRightarrow{}  P[[]])


By

---

Latex:
((Unfold  `safety`  0  THEN  Auto)  THEN  ExRepD)

---

Home Index