---

Step * 1 2 1 of Lemma pair-sq-axiom-wf


1. a : Base
2. a1 : Base
3. a = a1 ∈ Top
4. b : Base
5. b1 : Base
6. b = b1 ∈ Top
7. ∀x,y:Base.  ((<x, y> ~ Ax) ⇒ False)
⊢ (<a, b> ~ Ax) = (<a1, b1> ~ Ax) ∈ Type
BY
{ TACTIC:(PromoteHyp (-1) 1
          THEN Auto
          THEN Refine_sqequalExtensionalEquality
          THEN D 0
          THEN Auto
          THEN FHyp 1 [-1]
          THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Base
2.  a1  :  Base
3.  a  =  a1
4.  b  :  Base
5.  b1  :  Base
6.  b  =  b1
7.  \mforall{}x,y:Base.    ((<x,  y>  \msim{}  Ax)  {}\mRightarrow{}  False)
\mvdash{}  (<a,  b>  \msim{}  Ax)  =  (<a1,  b1>  \msim{}  Ax)


By

---

Latex:
TACTIC:(PromoteHyp  (-1)  1
                THEN  Auto
                THEN  Refine\_sqequalExtensionalEquality
                THEN  D  0
                THEN  Auto
                THEN  FHyp  1  [-1]
                THEN  Auto)

---

Home Index