proposition: Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone.
proof: Proof. intros [index0 contents0] F. case F. - unfold empty,index,get,contents;intros;apply Tget_Tempty. - unfold push,index,get;simpl @contents. intros a S. rewrite Tget_Tadd. rewrite Psucc_Gt. intro W. change (get (Pos.succ (index S)) S =PNone). apply get_Full_Gt; auto. apply Psucc_Gt. Qed.
imports: List BinPos