proposition: Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty.
proof: Proof. intros [ind cont] F one; inversion F. - reflexivity. - simpl @index in one;assert (h:=Pos.succ_not_1 (index S)). congruence. Qed.
imports: List BinPos