proposition: Lemma right_identity : forall a : E, strong_axioms a -> compose a (identity (source 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 source_create. tv. ir. unfold identity in |- *; rewrite ev_create. tv. unfold identity in H0; rewrite source_create in H0. am. Qed.
imports: Arith functions