---

Step * of Lemma map-sig_wf

∀[Key,Value:Type].  (map-sig{i:l}(Key;Value) ∈ 𝕌')
BY
{ ((UnivCD THENA Auto)
   THEN UnfoldAtAddr [2] 0
   THEN Repeat (((MemCD THEN AddHiddenLabel `wf`) THENL [Id; D(-1) THEN Auto; Auto]))
   THEN Auto
   THEN Try (Complete ((UseWitness ⌈"x"⌉⋅ THEN Auto)))) }

---

Latex:


\mforall{}[Key,Value:Type].    (map-sig\{i:l\}(Key;Value)  \mmember{}  \mBbbU{}')


By

((UnivCD  THENA  Auto)
  THEN  UnfoldAtAddr  [2]  0
  THEN  Repeat  (((MemCD  THEN  AddHiddenLabel  `wf`)  THENL  [Id;  D(-1)  THEN  Auto;  Auto]))
  THEN  Auto
  THEN  Try  (Complete  ((UseWitness  \mkleeneopen{}"x"\mkleeneclose{}\mcdot{}  THEN  Auto))))

---

Home Index