Equiv (fun (Not g) -> (Not (fun b -> g (L b)), Not (fun c -> g (R c))), fun ((Not h), (Not g)) -> Not function
  | (L y) -> h y
  | (R a) -> h (g a))