---

Step * 8 of Lemma istype-inr-sqeq-inl


1. a1 : Base
2. b1 : Base
3. c : a1 = b1 ∈ Top
4. a : Base
5. b2 : Base
6. c1 : a = b2 ∈ Top
7. inr b2  ~ inl b1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr a  ~ inl b1
BY
{ ((InstHyp [⌜b1⌝;⌜b2⌝] (-1)⋅ THENA Auto) THEN D -1 THEN RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a1  :  Base
2.  b1  :  Base
3.  c  :  a1  =  b1
4.  a  :  Base
5.  b2  :  Base
6.  c1  :  a  =  b2
7.  inr  b2    \msim{}  inl  b1
8.  \mforall{}[a,b:Base].    (\mneg{}(inl  a  \msim{}  inr  b  ))
\mvdash{}  inr  a    \msim{}  inl  b1


By

---

Latex:
((InstHyp  [\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index