cases (in_sub_eq d p t1); simplify;
[1:generalize in match H3; clear H3; cases s (r Hr); clear s;
simplify; intros (Ert1); generalize in match Hr; clear Hr;
rewrite > Ert1; clear Ert1; clear r; intros (Ht1);
cases (in_sub_eq d p t1); simplify;
[1:generalize in match H3; clear H3; cases s (r Hr); clear s;
simplify; intros (Ert1); generalize in match Hr; clear Hr;
rewrite > Ert1; clear Ert1; clear r; intros (Ht1);