proposition: Theorem mkGH_incl: incl H.(s) mkGH.
proof: Proof. assert (H1: forall l, incl l H.(s) -> incl l (mkList G.(s) l)). intros l; elim l; simpl; auto with datatypes. intros a l1 H1 H2. case (In_dec A_dec a (mkList (s G) l1)); auto with datatypes. intros H3; assert (H4: incl l1 (mkList (s G) l1)). apply H1; auto with datatypes. intros b H4; apply H2; auto with datatypes. intros b; simpl; intros [H5 | H5]; subst; auto. intros _ b; simpl; intros [H3 | H3]; subst; auto. apply in_or_app; left. cut (In H.(e) G.(s)). elim (s G); simpl; auto. intros c l2 Hl2 [H3 | H3]; subst; sauto. assert (In b H.(s)); sauto. apply (H2 b); auto with datatypes. rewrite same_e_for_H_and_G; sauto. apply in_or_app; right. apply H1; auto with datatypes. 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