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