proposition: Lemma CompH_NT_assoc : (T o_NTh T') o_NTh T'' =_NTH T o_NTh T' o_NTh T''.
proof: Proof. unfold EqualH_NT, CompH_NT in |- *; simpl in |- *. unfold Ast in |- *; simpl in |- *. unfold Comp_FOb in |- *. unfold FMor at 4 in |- *; simpl in |- *. unfold Comp_FMor in |- *. intro a. apply Build_Equal_hom. apply Trans with (T'' (F' (F a)) o FMor G'' (T' (F a)) o FMor G'' (FMor G' (T a))). apply Comp_l; apply FComp. apply Ass. Qed.
imports: CatFunct