---

Step * 1 of Lemma set_car_inc


1. s : LOSet@i'
2. g : OGrp@i'
3. ps : (|s| × |g|+) List@i
4. ↑sd_ordered(map(λx.(fst(x));ps))@i
5. ¬↑(e ∈b map(λx.(snd(x));ps))@i
⊢ ¬↑(e ∈b map(λx.(snd(x));ps))
BY
{ (NthHypSq (-1) THEN RepUR ``mem mon_for for tlambda`` 0 THEN EqCD)⋅ }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  ps  :  (|s|  \mtimes{}  |g|\msupplus{})  List@i
4.  \muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps))@i
5.  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps))@i
\mvdash{}  \mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps))


By

---

Latex:
(NthHypSq  (-1)  THEN  RepUR  ``mem  mon\_for  for  tlambda``  0  THEN  EqCD)\mcdot{}

---

Home Index