Rewrite <- H8 in H1; Rewrite <- H8 in H2;
Rewrite <- H8 in H3; Rewrite <- H8 in H4; Clear H8 b.
IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
Rewrite <- H8 in H1; Rewrite <- H8 in H2;
Rewrite <- H8 in H3; Rewrite <- H8 in H4; Clear H8 b.
IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.