Using `refine` tactic to generate subgoals, but Coq complains when solving subgoals.

RefineWeird.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
*)

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 => _
            | EvDRec n Hn => _
            end).
  - apply H0.
  - apply H1.
    apply F.
    destruct Hn.
    apply H.
    apply Hn.
Qed.

(* Error:
Recursive definition of F is ill-formed.
In environment
P : nat -> Prop
H0 : P 0
H1 : forall n : nat, P n -> ev_dumb n /\ n <> 1 -> P (S (S n))
F : forall n : nat, ev_dumb n -> P n
n : nat
e : ev_dumb n
n0 : nat
Hn : ev_dumb n0 /\ n0 <> 1
Recursive call to F has principal argument equal to "n0" instead of a subterm of "n".
Recursive definition is:
"fun (n : nat) (e : ev_dumb n) =>
 match e in (ev_dumb n0) return (P n0) with
 | EvDBase => H0
 | EvDRec n0 Hn => H1 n0 (F n0 match Hn with
                               | conj H _ => H
                               end) Hn
 end".

 *)