Step
*
1
of Lemma
oal_mon_wf
1. a : LOSet@i'
2. b : AbDMon@i'
⊢ IsEqFun(|oal(a;b)|;=b)
BY
{ (Assert ⌜oal(a;b) ∈ DSet⌝⋅ THEN Auto THEN AddProperties (-1)⋅ THEN Auto)⋅ }
Latex:
Latex:
1. a : LOSet@i'
2. b : AbDMon@i'
\mvdash{} IsEqFun(|oal(a;b)|;=\msubb{})
By
Latex:
(Assert \mkleeneopen{}oal(a;b) \mmember{} DSet\mkleeneclose{}\mcdot{} THEN Auto THEN AddProperties (-1)\mcdot{} THEN Auto)\mcdot{}
Home
Index