---

Step * of Lemma face-maps-comp_wf

∀[L:(Cname × ℕ2) List]. ∀[I:Cname List].  (face-maps-comp(L) ∈ name-morph(map(λp.(fst(p));L) @ I;I))
BY
{ (InductionOnList THEN Unfold `face-maps-comp` 0 THEN Reduce 0 THEN Try (Fold `face-maps-comp` 0)) }

1
∀[I:Cname List]. (λt.t ∈ name-morph(I;I))

2
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))

---

Latex:

---

Latex:
\mforall{}[L:(Cname  \mtimes{}  \mBbbN{}2)  List].  \mforall{}[I:Cname  List].    (face-maps-comp(L)  \mmember{}  name-morph(map(\mlambda{}p.(fst(p));L)  @  I;I))


By

---

Latex:
(InductionOnList  THEN  Unfold  `face-maps-comp`  0  THEN  Reduce  0  THEN  Try  (Fold  `face-maps-comp`  0))

---

Home Index