proposition: Lemma right_fidentity : forall a f, axioms f -> a = source f -> fcompose f (fidentity a) = f.
proof: Proof. ir. rw H0; clear H0. ap axioms_extensionality; ir. fw'. am. fw. fw. rwi source_fcompose H0. rwi source_fidentity H0. fw'. Qed.
imports: Arith category