proposition: Lemma OT_sum_assoc1 r g r' g': order r -> substrate r = domain g -> order_type_fam g -> order r' -> substrate r' = domain g' -> order_fam g' -> r = order_sum r' g' -> let order_sum_assoc_aux := fun l => OT_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in OT_sum r g = OT_sum r' (Lg (domain g') (order_sum_assoc_aux)).
proof: Proof. move=> wor sr alB wor' sr' alw oal osa. rewrite /OT_sum. have oa': orsum_ax r' g' by []. apply: order_type_unique. set g'' := (Lg (domain g) (fun z => order_type_of (Vg g z))). have oa: orsum_ax r g''. rewrite /g'';red;aw; split => //;hnf; aw; move=> i idg; rewrite !LgV//. by move: (OT_prop3 (OT_prop2 (alB _ idg))). move: (orsum_assoc_iso oa oa' oal) => /=. set aux' := fun l => order_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g'' (J i l))). set f:= Lf _ _ _. move => oi1; move: (oi1) => [o1 o2 _ _]. apply: (@orderIT (order_sum r' (Lg (domain g') aux'))); first by exists f. apply: orsum_invariant2 =>//; aww. rewrite sr';move=> i isr; rewrite !LgV//; rewrite /osa /OT_sum; aw. set s := order_sum _ _. have os: order s. rewrite /s; apply: orsum_or; split => //; aw;trivial; first by apply: alw. hnf; aw;move=> j js; rewrite !LgV//. have jdg: inc (J j i) (domain g). by rewrite - sr oal (orsum_sr oa'); apply: disjoint_union_pi1. apply: (OT_prop3 (OT_prop2 (alB _ jdg))). have -> : (aux' i = s). rewrite /aux' /s; apply: f_equal. apply: Lg_exten => //;move=> j js. have pd: inc (J j i) (domain g). by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. rewrite /g'' ! LgV//. by rewrite OT_prop4 //; apply: order_type_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)