Require Export CFLib Main_ml.
Require Import Auxi_ml Auxi_proof Extra.

Lemma g_spec : 
  Spec g (x:int) |R>> R \[] (fun y => \[same x y]).
Proof.
  xcf. intros. xapp. hsimpl~. 
Qed.

Hint Extern 1 (RegisterSpec g) => Provide g_spec.