proposition: Lemma get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
proof: Proof. intros A t i j a Hij. destruct t as ((t, d), l). unfold set, get, length. case (l <=? i). reflexivity. rewrite P.F.add_neq_o. reflexivity. intro H; apply Hij; clear Hij. rewrite eqb_spec in H. assumption. Qed.
imports: Int63 Psatz ZArith