---

Step * of Lemma kind-rename-inj

∀[ra,rt:Id ─→ Id].  (Inj(Knd;Knd;λk.kind-rename(ra;rt;k))) supposing (Inj(Id;Id;ra) and Inj(Id;Id;rt))
BY
{ (Unfolds ``inject kind-rename`` 0
   THEN Reduce 0
   THEN Auto
   THEN AllHyps KindCase
   THEN Try (((FLemma `not_locl_rcv` [(-1)]) THEN Auto))
   THEN Try (((FLemma `not_rcv_locl` [(-1)]) THEN Auto))
   THEN Try (((FLemma `locl_one_one` [(-1)]) THEN Auto))
   THEN Try (((FLemma `rcv_one_one` [(-1)]) THEN Auto))
   THEN EqCD
   THEN Auto
   THEN AllHyps h.(BHyp h THEN Complete (Auto)) ) }

---

Latex:


\mforall{}[ra,rt:Id  {}\mrightarrow{}  Id].
    (Inj(Knd;Knd;\mlambda{}k.kind-rename(ra;rt;k)))  supposing  (Inj(Id;Id;ra)  and  Inj(Id;Id;rt))


By

(Unfolds  ``inject  kind-rename``  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AllHyps  KindCase
  THEN  Try  (((FLemma  `not\_locl\_rcv`  [(-1)])  THEN  Auto))
  THEN  Try  (((FLemma  `not\_rcv\_locl`  [(-1)])  THEN  Auto))
  THEN  Try  (((FLemma  `locl\_one\_one`  [(-1)])  THEN  Auto))
  THEN  Try  (((FLemma  `rcv\_one\_one`  [(-1)])  THEN  Auto))
  THEN  EqCD
  THEN  Auto
  THEN  AllHyps  h.(BHyp  h  THEN  Complete  (Auto))  )

---

Home Index