Step
*
1
of Lemma
pair-sq-axiom-wf
1. a : Top
2. b : Top
⊢ <a, b> ~ Ax ∈ Type
BY
{ TACTIC:Assert ⌜∀x,y:Base.  ((<x, y> ~ Ax) 
⇒ False)⌝⋅ }
1
.....assertion..... 
1. a : Top
2. b : Top
⊢ ∀x,y:Base.  ((<x, y> ~ Ax) 
⇒ False)
2
1. a : Top
2. b : Top
3. ∀x,y:Base.  ((<x, y> ~ Ax) 
⇒ False)
⊢ <a, b> ~ Ax ∈ Type
Latex:
Latex:
1.  a  :  Top
2.  b  :  Top
\mvdash{}  <a,  b>  \msim{}  Ax  \mmember{}  Type
By
Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x,y:Base.    ((<x,  y>  \msim{}  Ax)  {}\mRightarrow{}  False)\mkleeneclose{}\mcdot{}
Home
Index