fact: Definition Comp_One_mor (a : One_ob) := let () as x return (forall b c : One_ob, One_mor_setoid x b -> One_mor_setoid b c -> One_mor_setoid x c) := a in fun b c => let () as x return (One_mor_setoid Obone b -> One_mor_setoid b x -> One_mor_setoid Obone x) := c in fun _ _ => Id_Obone.
imports: Category