---

Step * of Lemma per-int_wf

per-int() ∈ Type
BY
{ (PerEqCD⋅ THEN Auto) }

1
1. x : Base
2. y : Base
3. z : uand(x ~ y;isint(x) ~ tt)
⊢ uand(y ~ x;isint(y) ~ tt)

2
1. x : Base
2. y : Base
3. z : Base
4. u : uand(x ~ y;isint(x) ~ tt)
5. v : uand(y ~ z;isint(y) ~ tt)
⊢ uand(x ~ z;isint(x) ~ tt)

---

Latex:

---

Latex:
per-int()  \mmember{}  Type


By

---

Latex:
(PerEqCD\mcdot{}  THEN  Auto)

---

Home Index