proposition: Lemma get_In : forall (x:A) (S:Store) (F:Full S) i , get i S = PSome x -> In x S F.
proof: Proof. induction F. - intro i;rewrite get_empty; congruence. - intro i;rewrite get_push_Full;trivial. case_eq (i ?= index S);simpl. + left;congruence. + right;eauto. + congruence. Qed.
imports: List BinPos