Repeat IH d a0 a; Clear H H1 c t1 t2.
Subst1GenBase; SymEqual; LiftGenBase; Rewrite H in H8; Rewrite H11 in H1; Rewrite H12 in H7; Clear H H11 H12 x1 x4 x5.
Subst1Confluence; Rewrite H in H8; Clear H x6.
EApply ex3_2_intro; Try Rewrite lift_flat;
[ Idtac | EApply subst1_tail; [ Idtac | Rewrite lift_bind ] | Idtac ]; XEAuto.
Repeat IH d a0 a; Clear H H1 c t1 t2.
Subst1GenBase; SymEqual; LiftGenBase; Rewrite H in H8; Rewrite H11 in H1; Rewrite H12 in H7; Clear H H11 H12 x1 x4 x5.
Subst1Confluence; Rewrite H in H8; Clear H x6.
EApply ex3_2_intro; Try Rewrite lift_flat;
[ Idtac | EApply subst1_tail; [ Idtac | Rewrite lift_bind ] | Idtac ]; XEAuto.