proposition: Theorem incl_mkGH: incl mkGH H.(s).
proof: Proof. assert (H1: forall l, incl l H.(s) -> incl (mkList G.(s) l) H.(s)). intros l; elim l; simpl; auto with datatypes. intros a l1 H1 H2. case (In_dec A_dec a (mkList (s G) l1)); intros H3; auto with datatypes. apply H1; apply incl_tran with (2 := H2); auto with datatypes. apply incl_app. intros b H4. case ListAux.in_map_inv with (1:= H4); auto. intros c (Hc1, Hc2); subst; sauto. apply internal; auto with datatypes. apply H1; apply incl_tran with (2 := H2); auto with datatypes. unfold mkGH; apply H1; auto with datatypes. Qed.
imports: List UList ListAux ZArith Znumtheory NatAux FGroup