---

Step * of Lemma ctt-opr-is-implies

No Annotations
∀[f:CttOp]. ∀[s:Atom].  f ~ <"opid", s> supposing ↑ctt-opr-is(f;s)
BY
{ Auto }

1
1. f : CttOp
2. s : Atom
3. ↑ctt-opr-is(f;s)
⊢ f = <"opid", s> ∈ (Atom × Atom)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[f:CttOp].  \mforall{}[s:Atom].    f  \msim{}  <"opid",  s>  supposing  \muparrow{}ctt-opr-is(f;s)


By

---

Latex:
Auto

---

Home Index