---

Step * of Lemma face-map_wf2

∀[I:Cname List]. ∀[x:Cname]. ∀[p:ℕ2].  ((x:=p) ∈ name-morph(I;I-[x]))
BY
{ (Auto THEN Assert ⌜l_subset(Cname;I;[x / I-[x]])⌝⋅) }

1
.....assertion..... 
1. I : Cname List
2. x : Cname
3. p : ℕ2
⊢ l_subset(Cname;I;[x / I-[x]])

2
1. I : Cname List
2. x : Cname
3. p : ℕ2
4. l_subset(Cname;I;[x / I-[x]])
⊢ (x:=p) ∈ name-morph(I;I-[x])

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x:Cname].  \mforall{}[p:\mBbbN{}2].    ((x:=p)  \mmember{}  name-morph(I;I-[x]))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}l\_subset(Cname;I;[x  /  I-[x]])\mkleeneclose{}\mcdot{})

---

Home Index