Inversion H0; CSubst0Drop.
Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
Clear H0 H10 H11 H12 x0 x1 x2.
DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
IHT; EApply ty0_conv;
[ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
Clear H0 H10 H11 H12 x0 x1 x2.
DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
IHT; EApply ty0_conv;
[ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.