Remove broken code-path in product param atomization of `destruct`
Remove broken code-path in product param atomization of `destruct`

`Tactics.atomize_param_of_ind_then` thinks that it has the ability to atomize
parameters inside of products. This code-path is at least partially broken.
I also believe that there is no way to exercise this code-path in a
non-trivial way that does not generate anomalies. (In other words: I think it is
dead code.) Hence we remove it.

Testcase:
```
Inductive test : unit -> Prop :=.
Definition test2 := forall x, test x.
Lemma t (H : test2) : True.
edestruct H using test_rect.
Abort.
(* Used to error with:
Unbound reference: In environment
H, t : test2
The reference 1 is free.

Now errors with:
Not an inductive definition.
*)
```

SkySkimmer/coq,SkySkimmer/coq,ejgallego/coq,coq/coq,SkySkimmer/coq,Zimmi48/coq,Zimmi48/coq,Zimmi48/coq,coq/coq,SkySkimmer/coq,coq/coq,ejgallego/coq,ejgallego/coq,ejgallego/coq,Zimmi48/coq,coq/coq