proposition: Lemma fa_extensionality : forall u v, inc u (function_arrow_set (source u) (target u)) -> inc v (function_arrow_set (source v) (target v)) -> source u = source v -> target u = target v -> (forall x, inc x (source u) -> V x (arrow u) = V x (arrow v)) -> u = v.
proof: Proof. ir. rwi inc_function_arrow_set H; rwi inc_function_arrow_set H0; ee. uh H; uh H0. rw H. rw H0. rw H1. rw H2. ap uneq. ap function_extensionality. am. am. ir. ufi defined H16. ee. uhg; ee. am. rwi H13 H17. rw H7. wrr H1. ir. ufi defined H16. ee. uhg; ee. am. rwi H7 H17. rw H13. rww H1. ir. ap H3. uh H16; ee. wrr H13. Qed.
imports: Arith ordinal nat_trans