proposition: Theorem FELLK_in: forall e, In e FELLK.
proof: Proof. intros e; case e; unfold FELLK; simpl; auto. intros x y H; right; apply mk_lelt_in_rev. apply ELK_complete; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith