let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds index p = index (SepVar p)
let p be Element of CQC-WFF A; :: thesis: index p = index (SepVar p)
still_not-bound_in p = still_not-bound_in (SepVar p) by Th44;
hence index p = index (SepVar p) ; :: thesis: verum