proposition: Theorem isupport_aux_ulist: forall l, ulist l -> ulist (isupport_aux l).
proof: Proof. intros l; elim l; simpl; auto with datatypes. intros a l1 H1 H2; case_eq (is_inv a); intros H3; auto with datatypes. apply ulist_cons; auto with datatypes. intros H4; apply (ulist_app_inv _ (a::nil) l1 a); auto with datatypes. apply (isupport_aux_incl l1 a); auto. apply H1; apply ulist_app_inv_r with (a:: nil); auto. apply H1; apply ulist_app_inv_r with (a:: nil); auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup