let p be Element of CQC-WFF ; :: thesis: index p = index (SepVar p)
still_not-bound_in p = still_not-bound_in (SepVar p) by Th45;
hence index p = index (SepVar p) ; :: thesis: verum