---

Step * of Lemma C_LVALUE-proper-Scomped

∀env:C_TYPE_env(). ∀lval:C_LVALUE(). ∀a:Atom.
  ((↑C_LVALUE-proper(env;LV_Scomp(lval;a))) ⇒ (↑C_Struct?(outl(C_TYPE-of-LVALUE(env;lval)))))
BY
{ ((Auto THEN InstLemma `C_LVALUE-proper-Scomp` [⌈env⌉;⌈LV_Scomp(lval;a)⌉]⋅)
   THEN Try (Complete (Auto))
   THEN RepUR ``let`` -1
   THEN Auto)⋅ }

---

Latex:


\mforall{}env:C\_TYPE\_env().  \mforall{}lval:C\_LVALUE().  \mforall{}a:Atom.
    ((\muparrow{}C\_LVALUE-proper(env;LV\_Scomp(lval;a)))  {}\mRightarrow{}  (\muparrow{}C\_Struct?(outl(C\_TYPE-of-LVALUE(env;lval)))))


By

((Auto  THEN  InstLemma  `C\_LVALUE-proper-Scomp`  [\mkleeneopen{}env\mkleeneclose{};\mkleeneopen{}LV\_Scomp(lval;a)\mkleeneclose{}]\mcdot{})
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``let``  -1
  THEN  Auto)\mcdot{}

---

Home Index