+lemma value_head : ∀a,l,i.Qpos i ≤ \fst a → value_simple (a::l) i = \snd a.
+intros; unfold value_simple; unfold match_domain; cases (cases_find bar (match_pred i) (a::l) ▭);
+[1: cases i1 in H2 H3 H4; intros; [reflexivity] lapply (H4 O) as K; [2: apply le_S_S; apply le_O_n;]
+ simplify in K; unfold match_pred in K; cases (q_cmp (Qpos i) (\fst a)) in K;
+ simplify; intros; [destruct H6] lapply (q_le_lt_trans ??? H H5) as K; cases (q_lt_corefl ? K);
+|2: cases (?:False); lapply (H3 0); [2: simplify; apply le_S_S; apply le_O_n;]
+ unfold match_pred in Hletin; simplify in Hletin; cases (q_cmp (Qpos i) (\fst a)) in Hletin;
+ simplify; intros; [destruct H5] lapply (q_le_lt_trans ??? H H4); apply (q_lt_corefl ? Hletin);]
+qed.
+
+lemma value_unit : ∀x,i. value_simple [x] i = \snd x.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) [x] ▭);
+[1: cases i1 in H; intros; [reflexivity] simplify in H;
+ cases (not_le_Sn_O ? (le_S_S_to_le ?? H));
+|2: simplify in H; destruct H; reflexivity;]
+qed.