Coq auto-generated induction principles being silly.

InductionPls.v

Inductive ev_dumb : nat -> Prop :=
  | EvDBase : ev_dumb 0
  | EvDRec  : forall n, ev_dumb n /\ n <> 1 -> ev_dumb (S (S n)).

Check ev_dumb_ind.

(* ev_dumb_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, ev_dumb n /\ n <> 1 -> P (S (S n))) -> forall n : nat, ev_dumb n -> P n
*)

Inductive ev_dumb' : nat -> Prop :=
  | EvDBase' : ev_dumb' 0
  | EvDRec'  : forall n, ev_dumb' n -> n <> 1 -> ev_dumb' (S (S n)).

Check ev_dumb'_ind.

(* ev_dumb'_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, ev_dumb' n -> P n -> n <> 1 -> P (S (S n))) -> forall n : nat, ev_dumb' n -> P n
*)