---

Step * of Lemma istype-inr-sqeq-inl

∀[a,b:Top].  istype(inr b  ~ inl a)
BY
{ (TACTIC:Intros
   THEN At ⌜Type⌝ (D 0)⋅
   THEN PointwiseFunctionality 1
   THEN PointwiseFunctionality (-1)
   THEN Repeat (((EqCDA ORELSE Unfold `member` 0) THEN Try (Refine_sqequalExtensionalEquality)))
   THEN RepeatFor 3 ((D 0 THENW Auto))
   THEN InstLemma `not-inl-sqeq-inr` []
   THEN Auto
   THEN skip{((Unfold `not` -1 THEN FHyp (-1) [-2]) THEN Auto)}) }

1
1. a1 : Base
2. b1 : Base
3. c : a1 = b1 ∈ Top
4. a : Base
5. b2 : Base
6. c1 : a = b2 ∈ Top
7. inr a  ~ inl a1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr b2  ~ inl a1

2
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 a1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr a  ~ inl a1

3
1. a1 : Base
2. b1 : Base
3. c : a1 = b1 ∈ Top
4. a : Base
5. b2 : Base
6. c1 : a = b2 ∈ Top
7. inr a  ~ inl a1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr a  ~ inl b1

4
1. a1 : Base
2. b1 : Base
3. c : a1 = b1 ∈ Top
4. a : Base
5. b2 : Base
6. c1 : a = b2 ∈ Top
7. inr a  ~ inl b1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr a  ~ inl a1

5
1. a1 : Base
2. b1 : Base
3. c : a1 = b1 ∈ Top
4. a : Base
5. b2 : Base
6. c1 : a = b2 ∈ Top
7. inr a  ~ inl a1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr b2  ~ inl a1

6
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 a1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr a  ~ inl a1

7
1. a1 : Base
2. b1 : Base
3. c : a1 = b1 ∈ Top
4. a : Base
5. b2 : Base
6. c1 : a = b2 ∈ Top
7. inr a  ~ inl b1
8. ∀[a,b:Base].  (¬(inl a ~ inr b ))
⊢ inr b2  ~ inl b1

8
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

---

Latex:

---

Latex:
\mforall{}[a,b:Top].    istype(inr  b    \msim{}  inl  a)


By

---

Latex:
(TACTIC:Intros
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}
  THEN  PointwiseFunctionality  1
  THEN  PointwiseFunctionality  (-1)
  THEN  Repeat  (((EqCDA  ORELSE  Unfold  `member`  0)  THEN  Try  (Refine\_sqequalExtensionalEquality)))
  THEN  RepeatFor  3  ((D  0  THENW  Auto))
  THEN  InstLemma  `not-inl-sqeq-inr`  []
  THEN  Auto
  THEN  skip\{((Unfold  `not`  -1  THEN  FHyp  (-1)  [-2])  THEN  Auto)\})

---

Home Index