proposition: Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) -> (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e).
proof: Proof. intros g e1 He1 H2. apply trans_equal with (op e1 g.(e)); sauto. Qed.
imports: List UList Tactic ZArith