proposition: Lemma append_spec l r x : InT x (append l r) <-> InT x l \/ InT x r.
proof: Proof. revert r. append_tac l r; autorew; try tauto. - revert IHlr; case append_rr_match; [intros a y b | intros t Ht]; autorew; tauto. - revert IHlr; case append_bb_match; [intros a y b | intros t Ht]; autorew; tauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat