proposition: Lemma shiftOut_same_inv : forall s n v, shiftOut s n = Some (v, s) -> n = O.
proof: Proof. intuition. eapply to_list_nil_inv. eapply app_second_eq. eapply shiftOut_correct_inv. eauto. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia