proposition: Lemma composition_create : forall o m c i s, composition (create o m c i s) = L m (fun u => (L (Z m (fun v => source u = target v)) (c u))).
proof: Proof. ir. uf create. uf composition. drw. Qed.
imports: Arith universe