proposition: Theorem isupport_aux_incl: forall l, incl (isupport_aux l) l.
proof: Proof. intros l; elim l; simpl; auto with datatypes. intros a l1 H1; case (is_inv a); auto with datatypes. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup