The Coq mailing list

[<mtkhan AT risc.jku.at>]

Hi,

I have the following sketch of the premises of my proof.

...
Parameter add0: (list or_integer_float) -> Z -> Z -> Z.

Axiom add0_def : forall (e:(list or_integer_float)) (i:Z) (j:Z) ...
....

H0 : result =
     add0
       (Cons (Integer 5)
          (Cons (Real (33 / 10))
             (Cons (Integer 8) (Cons (Real (4 / 10)) (Cons (Integer 9)
Nil)))))
       0
       (length
          (Cons (Integer 5)
             (Cons (Real (33 / 10))
                (Cons (Integer 8)
                   (Cons (Real (4 / 10)) (Cons (Integer 9) Nil))))))
...


And the goal is

result = 13%Z.

As a matter of fact the goal can easily be proved by just an application of
the function
add0 defined above. But it does not work for me. Can someone help me how we
can
prove such stuff, where we just need to compute the result of a function
application.

Thanks.

tk