proposition: Lemma Lp_sigma_tau_cone_law : Cone_law Lp_sigma_tau.
proof: Proof. unfold Cone_law, Lp_sigma_tau in |- *. intros i j g. apply Trans with (ApAphi_inv la (tau i o FMor G (FMor H g))). apply Aphi_invPres. apply (Eq_cone tau g). apply (Adj_eq5 la (FMor H g) (tau i)). Qed.
imports: Adj_UA Pres_Limits