proposition: Theorem get_Full_Gt : forall S, Full S -> forall i, (i ?= index S) = Gt -> get i S = PNone.
proof: Proof. intros S W;induction W. - unfold empty,index,get,contents;intros;apply Tget_Tempty. - unfold index,get,push. simpl @contents. intros i e;rewrite Tget_Tadd. rewrite (Gt_Psucc _ _ e). unfold get in IHW. apply IHW;apply Gt_Psucc;assumption. Qed.
imports: List BinPos