---

Step * of Lemma strong_safety_safety

∀[A:Type]. ∀[P:(A List) ⟶ ℙ].  (strong_safety(A;x.P[x]) ⇒ safety(A;x.P[x]))
BY
{ ((((Unfolds ``safety strong_safety`` 0 THEN Auto) THEN BackThruHyp'' 3) THEN Auto) THEN Easy) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:(A  List)  {}\mrightarrow{}  \mBbbP{}].    (strong\_safety(A;x.P[x])  {}\mRightarrow{}  safety(A;x.P[x]))


By

---

Latex:
((((Unfolds  ``safety  strong\_safety``  0  THEN  Auto)  THEN  BackThruHyp''  3)  THEN  Auto)  THEN  Easy)

---

Home Index