The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

>
> Why not just write a helper function with a type like this?
>     A -> forall P, is_A_formula P -> Prop
> Then you can pattern-match on the 3rd argument without any fuss.

Thanks! Worked perfectly:

Fixpoint helper a P (pf : is_A_formula P) := match pf with
| atom_formula _ _           => P
| and_formula  P Q pf_P pf_Q => helper (p0 a) P pf_P /\ helper (p1 a) Q pf_Q
end.

Definition realizes a (P : A_formulas) := let (P, pf) := P in helper a P pf.