---

Step * of Lemma per-union-elim

∀[A,B:Type].
  ∀x:per-union(A;B)
    per-or(uand(x ~ inl outl(x);outl(x) ∈ A supposing x ~ inl outl(x));uand(x ~ inr outr(x) ;outr(x) ∈ B 
                                                                                             supposing x 
                                                                                             ~ inr outr(x) ))
BY
{ (Auto THEN (InstLemma `per-union-elim1` [⌜A⌝;⌜B⌝;⌜x⌝]⋅ THENA Auto) THEN PerOrHD (-1)) }

1
.....aux..... 
1. A : Type
2. B : Type
3. x : per-union(A;B)
4. per-product(per-value();x@0.if x@0 = Ax then x ~ inl outl(x) otherwise x ~ inr outr(x) )
⊢ λx@0.if x@0 = Ax then x ~ inl outl(x) otherwise x ~ inr outr(x)  ∈ per-function(per-value();a.Type)

2
1. [A] : Type
2. [B] : Type
3. x : per-union(A;B)
4. x ~ inl outl(x)
⊢ per-or(uand(x ~ inl outl(x);outl(x) ∈ A supposing x ~ inl outl(x));uand(x ~ inr outr(x) ;outr(x) ∈ B 
                                                                                           supposing x ~ inr outr(x) ))

3
1. [A] : Type
2. [B] : Type
3. x : per-union(A;B)
4. x ~ inr outr(x) 
⊢ per-or(uand(x ~ inl outl(x);outl(x) ∈ A supposing x ~ inl outl(x));uand(x ~ inr outr(x) ;outr(x) ∈ B 
                                                                                           supposing x ~ inr outr(x) ))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}x:per-union(A;B)
        per-or(uand(x  \msim{}  inl  outl(x);outl(x)  \mmember{}  A  supposing  x  \msim{}  inl  outl(x));uand(x 
        \msim{}  inr  outr(x)  ;outr(x)  \mmember{}  B  supposing  x  \msim{}  inr  outr(x)  ))


By

---

Latex:
(Auto  THEN  (InstLemma  `per-union-elim1`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  PerOrHD  (-1))

---

Home Index