proposition: Lemma compose_ev : forall x f g : E, inc x (domain (compose f g)) -> V x (compose f g) = V (V x g) f.
proof: Proof. ir. unfold compose in |- *. unfold compose in H. rewrite create_domain in H. ap create_V_apply. am. tv. Qed.
imports: set_theory