---

Step * of Lemma pair-sq-axiom-wf

∀[a,b:Top].  (<a, b> ~ Ax ∈ Type)
BY
{ TACTIC:(UnivCD THENA Auto) }

1
1. a : Top
2. b : Top
⊢ <a, b> ~ Ax ∈ Type

---

Latex:

---

Latex:
\mforall{}[a,b:Top].    (<a,  b>  \msim{}  Ax  \mmember{}  Type)


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index