proposition: Lemma left_identity : forall a : E, strong_axioms a -> compose (identity (target a)) a = a.
proof: Proof. ir. unfold compose in |- *. ap realizes_like_eq. unfold strong_axioms in H; xe. unfold realizes in |- *. xe. unfold identity in |- *; rewrite target_create. tv. ir. unfold identity in |- *. rewrite ev_create. tv. unfold strong_axioms in H. xd. Qed.
imports: Arith functions