added v_inl v_inr as cbv-values

src/CBV.v

@@ -19,6 +19,14 @@ Inductive value : form -> Prop :=
       value t ->
       value s ->
       value (f_pair t s)
+  | v_inl : forall t,
+        is_term t ->
+        value t ->
+        value (f_inl t)
+  | v_inr : forall t,
+        is_term t ->
+        value t ->
+        value (f_inr t)
   | v_func : 
       forall x t,
         is_term t ->