2073 	$a :: rs \grewrites \hflataux{a} @ rs$

  2073 	$a :: rs \grewrites \hflataux{a} @ rs$

  2074 \end{lemma}

  2074 \end{lemma}

  2075 \begin{proof}

  2075 \begin{proof}

  2076 	By induction on $a$. $rs$ is set to take arbitrary values.

  2076 	By induction on $a$. $rs$ is set to take arbitrary values.

  2077 \end{proof}

  2077 \end{proof}

  2080 \begin{lemma}\label{cbsHfauRsimpeq1}

  2082 \begin{lemma}\label{cbsHfauRsimpeq1}

  2081 	$\rsimp{(r_1 + r_2)} = \rsimp{(\RALTS{\hflataux{r_1} @ \hflataux{r_2}})}$

  2083 	$\rsimp{(r_1 + r_2)} = \rsimp{(\RALTS{\hflataux{r_1} @ \hflataux{r_2}})}$

  2082 \end{lemma}

  2084 \end{lemma}

  2083 

  2085 

  2084 \begin{proof}

  2086 \begin{proof}