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