#alpha #sep #inc #i #outc #Hloop
lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%]
-Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
-[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
+[ whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
%
[ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
[#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
[#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
|*:% #H2 normalize in H2; destruct (H2) ]
]
-| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
+| #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH
#b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep *
[* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb %
#alpha #sep #inc #i #outc #Hloop
lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
-Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
-[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
+[ whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
%
[ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
[#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
[#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
|*:% #H2 normalize in H2; destruct (H2) ]
]
-| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
+| #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH
#b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep *
[* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb %