---

Step * of Lemma C_LVALUE-proper-Ground

∀env:C_TYPE_env(). ∀lval:C_LVALUE().
  ((↑LV_Ground?(lval)) ⇒ (↑C_LVALUE-proper(env;lval)) ⇒ (↑isl(env LV_Ground-loc(lval))))
BY
{ ((D 0 THENA Auto)
   THEN BLemma `C_LVALUE-induction`
   THEN RepUR ``let`` 0
   THEN Auto
   THEN OnMaybeHyp 6 (\h. ((RepUR ``C_LVALUE-proper C_TYPE-of-LVALUE`` h
                            THEN Fold `C_TYPE-of-LVALUE` h
                            THEN Fold `C_LVALUE-proper` h)
                           THEN Repeat ((SplitOnHypITE h  THEN Auto))
                           ))) }

---

Latex:


\mforall{}env:C\_TYPE\_env().  \mforall{}lval:C\_LVALUE().
    ((\muparrow{}LV\_Ground?(lval))  {}\mRightarrow{}  (\muparrow{}C\_LVALUE-proper(env;lval))  {}\mRightarrow{}  (\muparrow{}isl(env  LV\_Ground-loc(lval))))


By

((D  0  THENA  Auto)
  THEN  BLemma  `C\_LVALUE-induction`
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  ((RepUR  ``C\_LVALUE-proper  C\_TYPE-of-LVALUE``  h
                                                    THEN  Fold  `C\_TYPE-of-LVALUE`  h
                                                    THEN  Fold  `C\_LVALUE-proper`  h)
                                                  THEN  Repeat  ((SplitOnHypITE  h    THEN  Auto))
                                                  )))

---

Home Index