The Coq mailing list

["Wan Hai" <wan.whyhigh AT gmail.com>]

Deal all,

Here I have a function fc:
------------------------------
fc =
fix fc (n : nat) (c : nat -> nat) {struct n} : nat :=
  match n with
  | 0 => c 1
  | S n' => fc n' (fun v : nat => c (n * v))
  end
------------------------------
which is of type: nat -> (nat -> nat) -> nat.

I want to prove that:

forall m1 m2 n, fc n (fun x=>m1*m2*x) = fc n (fun x=>m2*m1*x)

It is obviously right. I proved this in Coq by "cut ((fun x=>m1*m2*x)
= (fun x=>m2*m1*x))" and then prove "(fun x=>m1*m2*x) = (fun
x=>m2*m1*x)" by an extensionality axiom of function which says that:
forall f g, (forall n, f n = g n) -> f = g.

Is there another way to prove this not using the extensionality axiom?

Thanks in advance!

-- 
Best regards,
Hai Wan