The Coq mailing list

["D. Pucci" <danpucci AT poczta.onet.pl>]

I am stuck with an apparently very simple prove:

=================================================
Parameter f: bool -> bool -> bool.

Definition p1 := fun a: bool => (if a then (f false) else (f true)) a.

Definition p2 := fun a: bool => if a then (f false a) else (f true a).

Theorem abc: p1 = p2.
=================================================

Shouldn't this be provable by reducing p1 and p2 to the same normal form?

Can anybody help me?

Thank you in advance.