proposition: Theorem get_push_Full : forall i a S, Full S -> get i (push a S) = match (i ?= index S) with Eq => PSome a | Lt => get i S | Gt => PNone end.
proof: Proof. intros i a S F. case_eq (i ?= index S). - intro e;rewrite (Pos.compare_eq _ _ e). destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd. rewrite Pos.compare_refl;reflexivity. - intros;destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd. simpl @index in H;rewrite H;reflexivity. - intro H;generalize H;clear H. unfold get,push;simpl. rewrite Tget_Tadd;intro e;rewrite e. change (get i S=PNone). apply get_Full_Gt;auto. Qed.
imports: List BinPos