proposition: Lemma mkX_ok p l : nth 0 p l == (mk_X p) @ l.
proof: Proof. destruct p;simpl;intros;Esimpl;trivial. - now rewrite <-jump_tl, nth_jump. - now rewrite <- nth_jump, nth_pred_double. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory