proposition: Theorem isupport_aux_is_in: forall l a, is_inv a = true -> In a l -> In a (isupport_aux l).
proof: Proof. intros l a; elim l; simpl; auto. intros b l1 Rec H [H1 | H1]; subst. rewrite H; auto with datatypes. case (is_inv b); auto with datatypes. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup