---

Step * 2 of Lemma face-maps-comp_wf


1. u : Cname × ℕ2
2. v : (Cname × ℕ2) List
3. ∀[I:Cname List]. (face-maps-comp(v) ∈ name-morph(map(λp.(fst(p));v) @ I;I))
⊢ ∀[I:Cname List]. ((let x,i = u in (x:=i) o face-maps-comp(v)) ∈ name-morph([fst(u) / (map(λp.(fst(p));v) @ I)];I))
BY
{ ((D 1 THEN Reduce 0) THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  Cname  \mtimes{}  \mBbbN{}2
2.  v  :  (Cname  \mtimes{}  \mBbbN{}2)  List
3.  \mforall{}[I:Cname  List].  (face-maps-comp(v)  \mmember{}  name-morph(map(\mlambda{}p.(fst(p));v)  @  I;I))
\mvdash{}  \mforall{}[I:Cname  List]
        ((let  x,i  =  u 
            in  (x:=i)  o  face-maps-comp(v))  \mmember{}  name-morph([fst(u)  /  (map(\mlambda{}p.(fst(p));v)  @  I)];I))


By

---

Latex:
((D  1  THEN  Reduce  0)  THEN  ParallelLast  THEN  Auto)

---

Home Index