proposition: Lemma get_set_same : forall A t i (a:A), (i <? length t) = true -> t.[i<-a].[i] = a.
proof: Proof. intros A t i a. destruct t as ((t, d), l). unfold set, get, length. intro Hi; generalize Hi. rewrite ltb_spec. rewrite Z.lt_nge. rewrite <- leb_spec. rewrite Bool.not_true_iff_false. intro Hi'; rewrite Hi'; clear Hi'. rewrite Hi; clear Hi. rewrite P.F.add_eq_o. reflexivity. rewrite eqb_spec. reflexivity. Qed.
imports: Int63 Psatz ZArith