+theorem iter_p_gen_iter_p_gen:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to
+(associative A plusA) \to
+(\forall a:A.(plusA a baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall x,y. x < n \to y < m \to
+ (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
+iter_p_gen n p11 A
+ (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
+ baseA plusA =
+iter_p_gen m p21 A
+ (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA )
+ baseA plusA.
+intros.
+apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
+ n m m n p11 p21 p12 p22)
+ [intros.split
+ [split
+ [split
+ [split
+ [split
+ [apply (andb_true_true ? (p12 j i)).
+ rewrite > H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ |apply (andb_true_true_r (p11 j)).
+ rewrite > H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ ]
+ |reflexivity
+ ]
+ |reflexivity
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ |intros.split
+ [split
+ [split
+ [split
+ [split
+ [apply (andb_true_true ? (p22 j i)).
+ rewrite < H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ |apply (andb_true_true_r (p21 j)).
+ rewrite < H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ ]
+ |reflexivity
+ ]
+ |reflexivity
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+qed.
\ No newline at end of file