proposition: Lemma Full_push_compat : forall i a S, Full S -> forall x, get i S = PSome x -> get i (push a S) = PSome x.
proof: Proof. intros i a S F x H. case_eq (i ?= index S);intro test. - rewrite (Pos.compare_eq _ _ test) in H. rewrite (get_Full_Eq _ F) in H;congruence. - rewrite <- H. rewrite (get_push_Full i a). + rewrite test;reflexivity. + assumption. - rewrite (get_Full_Gt _ F) in H;congruence. Qed.
imports: List BinPos