proposition: Lemma INV_init s1 s2 `(Ok s1, Ok s2) : INV (rev_elements s1) (rev_elements s2) nil.
proof: Proof. rewrite !rev_elements_rev. split; rewrite ?rev_involutive; auto; intros; now inA. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat