proposition: Lemma Ast_nt_law : NT_law Ast.
proof: Proof. unfold NT_law, Ast, Comp_Functor in |- *. unfold FMor at 1 in |- *; simpl in |- *. unfold FMor at 3 in |- *; simpl in |- *. unfold Comp_FMor in |- *. intros a b f. apply Trans with ((FMor F' (T a) o T' (G a)) o FMor G' (FMor G f)). apply Trans with (FMor F' (FMor F f) o FMor F' (T b) o T' (G b)). apply Comp_l; apply Sym; apply (Ast_eq b). apply Trans with (FMor F' (T a) o FMor F' (FMor G f) o T' (G b)). apply Trans with ((FMor F' (FMor F f) o FMor F' (T b)) o T' (G b)). apply Ass. apply Trans with ((FMor F' (T a) o FMor F' (FMor G f)) o T' (G b)). apply Comp_r. apply Trans with (FMor F' (FMor F f o T b)). apply FComp1. apply Trans with (FMor F' (T a o FMor G f)). apply FPres; apply NatCond. apply FComp. apply Ass1. apply Trans with (FMor F' (T a) o T' (G a) o FMor G' (FMor G f)). apply Comp_l; apply NatCond. apply Ass. apply Comp_r. apply (Ast_eq a). Qed.
imports: CatFunct