#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)
#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)
[#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
|*:% #H2 normalize in H2; destruct (H2) ]
]
[#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
|*:% #H2 normalize in H2; destruct (H2) ]
]
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 %
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)
#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)
[#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
|*:% #H2 normalize in H2; destruct (H2) ]
]
[#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
|*:% #H2 normalize in H2; destruct (H2) ]
]
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 %
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 %