---

Step * of Lemma assert-ctt-opr-is

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index