---

Step * 6 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. z : Base
10. ispair(x) ~ tt
11. ispair(y) ~ tt
12. (fst(x)) = (fst(y)) ∈ per-value()
13. (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A1 otherwise B1 supposing (fst(x)) = (fst(y)) ∈ per-value()
14. ispair(y) ~ tt
15. ispair(z) ~ tt
16. (fst(y)) = (fst(z)) ∈ per-value()
17. (snd(y)) = (snd(z)) ∈ if fst(y) = Ax then A1 otherwise B1 supposing (fst(y)) = (fst(z)) ∈ per-value()
⊢ Ax ∈ (snd(x)) = (snd(z)) ∈ if fst(x) = Ax then A1 otherwise B1 supposing (fst(x)) = (fst(z)) ∈ per-value()
BY
{ ((InstLemma `per-value-property` [⌜fst(x)⌝]⋅ THENA Auto)
   THEN DUand (-1)⋅
   THEN (Try (Eliminate ⌜fst(y)⌝⋅) THEN Try (QuickAuto))⋅) }

---

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.  z  :  Base
10.  ispair(x)  \msim{}  tt
11.  ispair(y)  \msim{}  tt
12.  (fst(x))  =  (fst(y))
13.  (snd(x))  =  (snd(y))  supposing  (fst(x))  =  (fst(y))
14.  ispair(y)  \msim{}  tt
15.  ispair(z)  \msim{}  tt
16.  (fst(y))  =  (fst(z))
17.  (snd(y))  =  (snd(z))  supposing  (fst(y))  =  (fst(z))
\mvdash{}  Ax  \mmember{}  (snd(x))  =  (snd(z))  supposing  (fst(x))  =  (fst(z))


By

---

Latex:
((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{})

---

Home Index