destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
[ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
[ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].