LARA

You could add the following rules:

\begin{equation*}\frac{\Gamma \vdash e_1: ID[] \qquad \Gamma \vdash e_2 : TInt}{\Gamma \vdash e_1[e_2] : T}\end{equation*}


\begin{equation*}\frac{\Gamma \vdash e_1: ID[]} {\Gamma \vdash e_1.length : TInt}\end{equation*}


\begin{equation*}\frac{\qquad \Gamma \vdash ID \in Classes \qquad \Gamma \vdash e : TInt}{\Gamma \vdash new\, ID[e] : ID[]}\end{equation*}


\begin{equation*}\frac{\Gamma \vdash e_1: ID1[] \qquad \Gamma \vdash e_2 : TInt \qquad \Gamma \vdash e_3 : ID2 \qquad ID2<:ID1}{\Gamma \vdash e_1[e_2] = e_3: TUnit}\end{equation*}


\begin{equation*}\frac{\Gamma \vdash e_1: ID1[] \qquad \Gamma \vdash e_2 : ID2[]}{\Gamma \vdash e_1 == e_2 : TBool}\end{equation*}


\begin{equation*}\frac{ID \in Classes}{ID[] <: ID[]}\end{equation*}