Step * 1 1 1 of Lemma name-morph-extend-id

.....truecase..... 
1. Cname List
2. nameset(I+)
3. fresh-cname(I) ∈ Cname
⊢ fresh-cname(I) ∈ extd-nameset(I+)
BY
(RevHypSubst' (-1) THEN Auto) }


Latex:


Latex:
.....truecase..... 
1.  I  :  Cname  List
2.  x  :  nameset(I+)
3.  x  =  fresh-cname(I)
\mvdash{}  x  =  fresh-cname(I)


By


Latex:
(RevHypSubst'  (-1)  0  THEN  Auto)




Home Index