---

Step * of Lemma safety_induced

∀[A,B:Type].  ∀f:A ⟶ B. ∀[P:(B List) ⟶ ℙ]. (safety(B;L.P[L]) ⇒ safety(A;L.P[map(f;L)]))
BY
{ (((Unfold `safety` 0 THEN Reduce 0) THEN Auto) THEN Using [`tr2',map(f;tr2)] BackThruSomeHyp THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. [P] : (B List) ⟶ ℙ
5. ∀tr1,tr2:B List.  (tr1 ≤ tr2 ⇒ P[tr2] ⇒ P[tr1])
6. tr1 : A List
7. tr2 : A List
8. tr1 ≤ tr2
9. P[map(f;tr2)]
⊢ map(f;tr1) ≤ map(f;tr2)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}[P:(B  List)  {}\mrightarrow{}  \mBbbP{}].  (safety(B;L.P[L])  {}\mRightarrow{}  safety(A;L.P[map(f;L)]))


By

---

Latex:
(((Unfold  `safety`  0  THEN  Reduce  0)  THEN  Auto)
  THEN  Using  [`tr2',map(f;tr2)]  BackThruSomeHyp
  THEN  Auto)

---

Home Index