The Coq mailing list

[Fritjof <fritjof AT uni-bremen.de>]

Hi,

I have the following theorem:
fun1 a = a' /\ fun2 b = b' <-> fun (x,y,z) = (x',y',z').

fun1 and fun2 are called inside the function fun:
fun(x,y,z)
 match fun1 a with
   | a' => match fun2 b with 
           | b' => (x',y',z') (* these values are calculated somehow *)
           | bb' => 
   | aa' => ...
 end 


I can show the following: fun1 a = a' /\ fun2 b = b' -> fun (x,y,z) = 
(x',y',z').  (the first part)

But not the second one: fun (x,y,z) = (x',y',z') -> fun1 a = a' /\ fun2 b = 
b'.
I didn't find a way to feed the left side of the implication into the 
hypothesis: fun (x,y,z) = (x',y',z').

Does someone has a hint for me how to solve this? 

Best regards,
--f.