∀I:Cname List. (I = [fresh-cname(I) / I]-[fresh-cname(I)] ∈ (Cname List))
{ Auto }
1. I : Cname List
⊢ I = [fresh-cname(I) / I]-[fresh-cname(I)] ∈ (Cname List)