proposition: Theorem inv_aux_in: forall l a, In (inv_aux l a) l \/ inv_aux l a = e.
proof: Proof. intros l a; elim l; simpl; auto. intros b l1; case (A_dec (op a b) e); case (A_dec (op b a) e); intros _ _ [H1 | H1]; auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup