proposition: Lemma left_fa_id : forall u x, inc u (function_arrow_set (source u) (target u)) -> x = target u -> fa_comp (fa_id x) u = u.
proof: Proof. ir. cp H. rwi inc_function_arrow_set H1. ee. ap fa_extensionality. ap inc_fas_fa_comp. rw source_fa_id. rw target_fa_id. ap inc_fas_fa_id. am. rww source_fa_id. rww source_fa_comp. rww target_fa_comp. am. rww source_fa_comp. rww target_fa_comp. rww target_fa_id. ir. rw V_fa_comp. rw V_fa_id. tv. ap inc_V_arrow2. am. rwi source_fa_comp H8. am. am. rw source_fa_id; rw target_fa_id. ap inc_fas_fa_id. am. rww source_fa_id. rwi source_fa_comp H8. am. Qed.
imports: Arith ordinal nat_trans