Require Import Recdef.

Inductive formula :=
| atom  : formula
| conn  : formula -> formula -> formula.

Fixpoint complexity P : nat := match P with
| atom     => 0
| conn P Q => Peano.max (complexity P) (complexity Q) + 1
end.

(* the following definition is OK: *)
Function truth P {measure complexity P} : Prop := match P with
| atom     => True
| conn P Q => truth P /\ truth Q
end.
Admitted.

(* the following definition gives the following output:

failure in proveterminate

Error: Found a product. Can not treat such a term
*)
Function truth' P {measure complexity P} : Prop := match P with
| atom     => True
| conn P Q => truth' P -> truth' Q
end.