---

Step * of Lemma ses-nonce-from-ordering

∀s:SES. (ActionsDisjoint ⇒ PropertyO ⇒ PropertyN)
BY
{ (Auto THEN (FLemma `ses-ordering-ordering\'` [2;3] THENA Auto)) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. PropertyO@i'
4. ses-ordering'(s)
⊢ PropertyN

---

Latex:

---

Latex:
\mforall{}s:SES.  (ActionsDisjoint  {}\mRightarrow{}  PropertyO  {}\mRightarrow{}  PropertyN)


By

---

Latex:
(Auto  THEN  (FLemma  `ses-ordering-ordering\mbackslash{}'`  [2;3]  THENA  Auto))

---

Home Index