proposition: Theorem mk_lelt_ulist: forall l H, ulist l -> ulist (mk_lelt l H).
proof: Proof. intros l; elim l; simpl; auto. intros (x, y) l1 Hrec H; simpl; auto. intros H1; inversion_clear H1. constructor; auto. intros H3; case H0; apply mk_lelt_in with (1 := H3). Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith