---

Step * of Lemma per-or-equal

∀[A1,B1,A2,B2:Type].  (per-or(A1;B1) = per-or(A2;B2) ∈ Type) supposing (A1 ≡ A2 and B1 ≡ B2)
BY
{ TACTIC:(Auto
          THEN RepUR ``per-or per-exists per-product`` 0
          THEN PerEqCD
          THEN Repeat (All DUand)
          THEN Try (QuickAuto)) }

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

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

3
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 A1 otherwise B1 supposing (fst(x)) = (fst(y)) ∈ per-value()
⊢ Ax ∈ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A2 otherwise B2 supposing (fst(x)) = (fst(y)) ∈ per-value()

4
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()

5
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 A1 otherwise B1 supposing (fst(x)) = (fst(y)) ∈ per-value()
⊢ Ax ∈ (snd(y)) = (snd(x)) ∈ if fst(y) = Ax then A1 otherwise B1 supposing (fst(y)) = (fst(x)) ∈ per-value()

6
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()

---

Latex:

---

Latex:
\mforall{}[A1,B1,A2,B2:Type].    (per-or(A1;B1)  =  per-or(A2;B2))  supposing  (A1  \mequiv{}  A2  and  B1  \mequiv{}  B2)


By

---

Latex:
TACTIC:(Auto
                THEN  RepUR  ``per-or  per-exists  per-product``  0
                THEN  PerEqCD
                THEN  Repeat  (All  DUand)
                THEN  Try  (QuickAuto))

---

Home Index