The first case of working full extraction. There are a number of things
that had to be changed to fit the RelationExtraction plugin:

Firstly the relations is_expr_of_expr and is_value_of_expr that are
generated and used to check for expressions and values respectively are
logical: they return Coq propositions that are in fact just a
conjunction of True and False. This does not get naturally extracted,
therefore I made an equivalent (proof TODO) pair of Fixpoints returning
booleans with names 
Firstly the relations xis_expr_of_expr and xis_value_of_expr
respectively. I am certain there must be a better way to do this.

Secondly, while the plugin is exceptionnaly good at extracting these
relation it requires explicit symbol casing. By this I mean the cases: 

 | JO_red_movebind : forall (e e'' e':expr),
     JO_red e e' ->
     JO_red (E_bind  (E_live_expr e)  e'') (E_bind  (E_live_expr e')
e'')

and     
     
 | JO_red_dobind : forall (v e:expr),
     is_value_of_expr v ->
     JO_red (E_bind  (E_live_expr v)  e) (E_apply e v)
     
are conflicting, because it is unable to figure out that JO_red e e'
implies that the equivalent v in the other would return false on
is_value_of_expr. This has to be modified to

 | JO_red_movebind : forall (e e'' e':expr),
     eq (xis_value_of_expr e) false ->
     JO_red e e' ->
     JO_red (E_bind  (E_live_expr e)  e'') (E_bind  (E_live_expr e')
e'')

and     
     
 | JO_red_dobind : forall (v e:expr),
     eq (xis_value_of_expr v) true ->
     JO_red (E_bind  (E_live_expr v)  e) (E_apply e v)

Which then get extracted as:   

| E_bind (E_live_expr e, e'') ->
    (match xis_value_of_expr e with
     | False ->
       (match jO_red1 e with
        | e' -> E_bind ((E_live_expr e'), e'')
        | _ -> assert false (*  *))
     | True -> E_apply (e'', e)
     | _ -> assert false (*  *))
     
     
This modified reduction operation has to be shown to be equivalent.

I wonder if there is a better way.