InductionPls.v

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

Lemma ev_dumb_ind' :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> ev_dumb n /\ n <> 1 -> P (S (S n))) ->
    forall n : nat, ev_dumb n -> P n.
Proof.
  intros P H0 H1.
  refine (fix F n e :=
          match e with
          | EvDBase => H0
          | EvDRec n c =>
            match c with
            | conj e' H => H1 _ (F _ e') c
            end
          end).
Qed.