---

Step * 1 1 of Lemma oal_dom_neg


1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
⊢ map(λz.(fst(z));ps) ≡(|a|) map(λz.(fst(z));--ps)
BY
{ ((StrengthenRel) THENA Auto) }

1
1. a : LOSet
2. b : AbDGrp
3. ps : |oal(a;b)|
⊢ map(λz.(fst(z));ps) = map(λz.(fst(z));--ps) ∈ (|a| List)

---

Latex:

---

Latex:

1.  a  :  LOSet
2.  b  :  AbDGrp
3.  ps  :  |oal(a;b)|
\mvdash{}  map(\mlambda{}z.(fst(z));ps)  \mequiv{}(|a|)  map(\mlambda{}z.(fst(z));--ps)


By

---

Latex:
((StrengthenRel)  THENA  Auto)

---

Home Index