Someone

void Lista<T>::eliminarPosicion(int pos){
    int i = 0, j = pos + 1;
    lista<T> listaAux;
	    //Estado inicialC1
		//vale this == pre(this) && listaAux == []  && i == 0 &&  0 <= pos <= |this|
    while(i < pos){
			//invariante: 0 <= i <= pos && this == pre(this) && listaAux == this[0..i)
			// variante pos - i;
 	    listaAux.agregarAtras(this.iesimo(i));
		i++;
	}
		//QC1: listaAux == pre(this)[o..pos)

		//estado LuegoC1
		//vale this == pre(this) 
		// vale QC1
		//Estado inicialC2
		//vale j == pos + 1 && listaAux == pre(this)[0..pos) && this == pre(this)
	while(j < this.longitud()){
			//invariante: pos  + 1 <= j <= |pre(this)| 
			//variante |pre(this)| - j
	    listaAux.agregarAtras(this.iesimo(j));
		j++;
	}
	
		//QC2: listaAux == pre(this)[0..pos) ++ pre(this)(pos.. |pre(this)|)
	this = listaAux;
	//vale this == pre(this)[0..pos) ++ pre(this)(pos.. |pre(this)|)
}