proposition: Lemma mor_comp : forall a b u v, mor a u -> mor a v -> source u = target v -> a = b -> mor a (comp b u v)= True.
proof: Proof. ir. wr H2. assert (composable_facts a u v). ap show_composable_facts; am. ap iff_eq; ir; try tv; try am. lu. Qed.
imports: Arith universe