---

Step * of Lemma add-remove-fresh-sq

∀I:Cname List. ([fresh-cname(I) / I]-[fresh-cname(I)] ~ I)
BY
{ ((UnivCD THENA Auto) THEN (InstLemma `add-remove-fresh-cname` [⌜I⌝]⋅ THENA Auto)) }

1
1. I : Cname List@i
2. I = [fresh-cname(I) / I]-[fresh-cname(I)] ∈ (Cname List)
⊢ [fresh-cname(I) / I]-[fresh-cname(I)] ~ I

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  ([fresh-cname(I)  /  I]-[fresh-cname(I)]  \msim{}  I)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (InstLemma  `add-remove-fresh-cname`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index