---

Step * of Lemma name-morph-extend-id

∀[I:Cname List]. ((1)+ = 1 ∈ name-morph(I+;I+))
BY
{ (Auto THEN Symmetry THEN BLemma `name-morphs-equal` THEN Auto) }

1
1. I : Cname List
⊢ 1 = (1)+ ∈ (nameset(I+) ⟶ extd-nameset(I+))

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  ((1)+  =  1)


By

---

Latex:
(Auto  THEN  Symmetry  THEN  BLemma  `name-morphs-equal`  THEN  Auto)

---

Home Index