proposition: Theorem EKa_in: forall l x y, ~ In x l -> ~ In (x, y) (EKa l).
proof: Proof. intros l x y; elim l; simpl; auto. intros a l1 Rec; case KLroot; auto. intros k Hk; case (Eth.(is_zero_correct) k); case is_zero. simpl; intros _ _ H1; case Hk; inversion_clear H1. injection H; intros; subst a; auto. case Rec; auto; case Hk; auto. simpl; intros _ H1 H2; inversion_clear H2; case Hk; auto. injection H; auto. case H; intros H2. injection H2; auto. case Rec; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith