---

Step * 4 of Lemma per-or-equal


1. A1 : Type
2. B1 : Type
3. A2 : Type
4. B2 : Type
5. B1 ≡ B2
6. A1 ≡ A2
7. x : Base
8. y : Base
9. ispair(x) ~ tt
10. ispair(y) ~ tt
11. (fst(x)) = (fst(y)) ∈ per-value()
12. (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A2 otherwise B2 supposing (fst(x)) = (fst(y)) ∈ per-value()
⊢ Ax ∈ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A1 otherwise B1 supposing (fst(x)) = (fst(y)) ∈ per-value()
BY
{ (ThinTrivial
   THEN ((InstLemma `per-value-property` [⌜fst(x)⌝]⋅ THENA Auto)
         THEN DUand (-1)⋅
         THEN (Try (Eliminate ⌜fst(y)⌝⋅) THEN Try (QuickAuto))⋅)⋅
   ) }

1
1. x : Base
2. A1 : Type
3. B1 : Type
4. A2 : Type
5. B2 : Type
6. B1 ≡ B2
7. A1 ≡ A2
8. y : Base
9. ispair(x) ~ tt
10. ispair(y) ~ tt
11. (fst(x)) = (fst(y)) ∈ per-value()
12. (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A2 otherwise B2
13. fst(x) ∈ Base
14. (fst(x))↓
⊢ Ax ∈ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A1 otherwise B1 supposing (fst(x)) = (fst(x)) ∈ per-value()

---

Latex:

---

Latex:

1.  A1  :  Type
2.  B1  :  Type
3.  A2  :  Type
4.  B2  :  Type
5.  B1  \mequiv{}  B2
6.  A1  \mequiv{}  A2
7.  x  :  Base
8.  y  :  Base
9.  ispair(x)  \msim{}  tt
10.  ispair(y)  \msim{}  tt
11.  (fst(x))  =  (fst(y))
12.  (snd(x))  =  (snd(y))  supposing  (fst(x))  =  (fst(y))
\mvdash{}  Ax  \mmember{}  (snd(x))  =  (snd(y))  supposing  (fst(x))  =  (fst(y))


By

---

Latex:
(ThinTrivial
  THEN  ((InstLemma  `per-value-property`  [\mkleeneopen{}fst(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  DUand  (-1)\mcdot{}
              THEN  (Try  (Eliminate  \mkleeneopen{}fst(y)\mkleeneclose{}\mcdot{})  THEN  Try  (QuickAuto))\mcdot{})\mcdot{}
  )

---

Home Index