---

Step * of Lemma iter_hdf_cons_lemma

∀bs,a,P:Top.  (P*([a / bs]) ~ fst(P(a))*(bs))
BY
{ (UnivCD THENA Auto) }

1
1. bs : Top@i
2. a : Top@i
3. P : Top@i
⊢ P*([a / bs]) ~ fst(P(a))*(bs)

---

Latex:


\mforall{}bs,a,P:Top.    (P*([a  /  bs])  \msim{}  fst(P(a))*(bs))


By

(UnivCD  THENA  Auto)

---

Home Index