Step
*
2
of Lemma
norm-runinfo_wf
1. M : Type ─→ Type
2. ∀P:Type. value-type(M[P])
3. y : Unit
⊢ inr ⋅ ∈ {info':pRunInfo(P.M[P])| info' = (inr y ) ∈ pRunInfo(P.M[P])}
BY
{ (MemTypeCD THEN Unfold `pRunInfo` 0 THEN Auto THEN EqCD THEN Auto) }
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. \mforall{}P:Type. value-type(M[P])
3. y : Unit
\mvdash{} inr \mcdot{} \mmember{} \{info':pRunInfo(P.M[P])| info' = (inr y )\}
By
Latex:
(MemTypeCD THEN Unfold `pRunInfo` 0 THEN Auto THEN EqCD THEN Auto)
Home
Index