proposition: Theorem ulist_mkGH: ulist mkGH.
proof: Proof. assert (H1: forall l, incl l H.(s) -> ulist (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)); intros H3; auto with datatypes. apply H1; apply incl_tran with (2 := H2); auto with datatypes. apply ulist_app; auto. apply ulist_map; sauto. intros x y H4 H5 H6; apply g_cancel_l with (g:= H) (a := a); sauto. apply H2; auto with datatypes. apply H1; apply incl_tran with (2 := H2); auto with datatypes. intros b H4 H5. case ListAux.in_map_inv with (1:= H4); auto. intros c (Hc, Hc1); subst. assert (H6: forall l a b, In b G.(s) -> incl l H.(s) -> In a (mkList G.(s) l) -> In (op a b) (mkList G.(s) l)). intros ll u v; elim ll; simpl; auto with datatypes. intros w ll1 T0 T1 T2. case (In_dec A_dec w (mkList (s G) ll1)); intros T3 T4; auto with datatypes. apply T0; auto; apply incl_tran with (2:= T2); auto with datatypes. case in_app_or with (1 := T4); intros T5; auto with datatypes. apply in_or_app; left. case ListAux.in_map_inv with (1:= T5); auto. intros z (Hz1, Hz2); subst. replace (op (op w z) v) with (op w (op z v)); sauto. apply in_map; sauto. apply assoc with H; auto with datatypes. apply in_or_app; right; auto with datatypes. apply T0; try apply incl_tran with (2 := T2); auto with datatypes. case H3; replace a with (op (op a c) (G.(i) c)); auto with datatypes. apply H6; sauto. apply incl_tran with (2 := H2); auto with datatypes. apply trans_equal with (op a (op c (G.(i) c))); sauto. apply sym_equal; apply assoc with H; auto with datatypes. replace (op c (G.(i) c)) with (G.(e)); sauto. rewrite <- same_e_for_H_and_G. assert (In a H.(s)); sauto; apply (H2 a); auto with datatypes. unfold mkGH; apply H1; auto with datatypes. Qed.
imports: List UList ListAux ZArith Znumtheory NatAux FGroup