proposition: Lemma twoarrow_nttyd_property : forall a u1 v1 u2 v2 r s, twoarrow_nt_hypothesis a u1 v1 u2 v2 r s -> nttyd_property (twoarrow_fun_data a u1 v1) (twoarrow_fun_data a u2 v2) (fun x : (obsy twoarrow_data) => match x with o1 => r | o2 => s end).
proof: Proof. ir. uh H; ee. assert (lem1: twoarrow_hypothesis a u1 v1). uhg; ee; am. assert (lem2: twoarrow_hypothesis a u2 v2). uhg; ee; am. uhg; ee. ap twoarrow_data_property. app twoarrow_fun_data_property. app twoarrow_fun_data_property. rw ft_twoarrow_fun_data; rww ft_twoarrow_fun_data. ir. rw ft_twoarrow_fun_data. nin x. am. am. ir. nin x. rww H6. rww H8. ir. nin x. rww H7. rww H9. ir. rw ft_twoarrow_fun_data. nin u. change (comp a r (id a (source u1)) = comp a (id a (source u2)) r). rww right_id. rww left_id. rww ob_source. rww ob_source. change (comp a s (id a (target u1)) = comp a (id a (target u2)) s). rww left_id. rww right_id. rww ob_target. rww ob_target. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits