Unnamed

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)|)
}



int posicion(const T & e) const {
int i = 0;
//Estado AntesC;
// vale i == 0 && e (pertenece) this && |this| >= 0
        while( i < this.length() && this.iesimo(i) != e) {
        
        //invariante I:  0 <= i <= |this| && ((paratodo) x <- [0.. i)) this [x] != e
        // variante v:|this| - i
        //Estado 1
        ++i;
        //Estado 2
 }

 
return i;
 //Estado DespuesC
//vale Q: cab([i| x <- [0.. |this|), this[x] == e])