---

Step * 3 of Lemma assert-C_TYPE_eq


∀to:C_TYPE()
  ((∀b:C_TYPE(). uiff(↑(C_TYPE_eq_fun(to) b);to = b ∈ C_TYPE()))
  ⇒ (∀b:C_TYPE(). uiff(↑(C_Pointer?(b) ∧b (C_TYPE_eq_fun(to) C_Pointer-to(b)));C_Pointer(to) = b ∈ C_TYPE())))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (BLemma `C_TYPE-induction` THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}to:C\_TYPE()
    ((\mforall{}b:C\_TYPE().  uiff(\muparrow{}(C\_TYPE\_eq\_fun(to)  b);to  =  b))
    {}\mRightarrow{}  (\mforall{}b:C\_TYPE().  uiff(\muparrow{}(C\_Pointer?(b)  \mwedge{}\msubb{}  (C\_TYPE\_eq\_fun(to)  C\_Pointer-to(b)));C\_Pointer(to)  =  b)))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (BLemma  `C\_TYPE-induction`  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index