whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse) ] -Hcomp1
cases (Hcomp2 … Hta_src Hta_dst) [ *
[ * #rs' * #Hxs #Hcurtc % %2 %{ls0} %{rs0} %{rs'} % // % //
| * #rs0' * #Hxs #Htc %2 >Htc %{ls0} %{rs0'} % // ]
| * #xs0 * #ci * #cj * #rs' * #rs0' * * *
#Hci #Hxs #Hrs0 #Htc @False_ind
whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse) ] -Hcomp1
cases (Hcomp2 … Hta_src Hta_dst) [ *
[ * #rs' * #Hxs #Hcurtc % %2 %{ls0} %{rs0} %{rs'} % // % //
| * #rs0' * #Hxs #Htc %2 >Htc %{ls0} %{rs0'} % // ]
| * #xs0 * #ci * #cj * #rs' * #rs0' * * *
#Hci #Hxs #Hrs0 #Htc @False_ind