Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
EApply ex2_intro; [ Idtac | EApply ty0_abbr; XEAuto ].
Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.
Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
EApply ex2_intro; [ Idtac | EApply ty0_abbr; XEAuto ].
Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.