proposition: Lemma vee_nttyd_property : forall a u1 v1 u2 v2 r s t, vee_nt_hypothesis a u1 v1 u2 v2 r s t -> nttyd_property (vee_fun_data a u1 v1) (vee_fun_data a u2 v2) (fun x : (obsy vee_data) => match x with o1 => r | o2 => s | o3 => t end).
proof: Proof. ir. uh H; ee. assert (lem1: vee_hypothesis a u1 v1). uhg; ee; am. assert (lem2: vee_hypothesis a u2 v2). uhg; ee; am. uhg; ee. ap vee_data_property. app vee_fun_data_property. app vee_fun_data_property. rw ft_vee_fun_data; rww ft_vee_fun_data. ir. rw ft_vee_fun_data. nin x. am. am. am. ir. nin x. rww H7. rww H9. rww H11. ir. nin x. rww H8. rww H10. rww H12. ir. rw ft_vee_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. change (comp a t (id a (source v1)) = comp a (id a (source v2)) t). rww left_id. rww right_id. rww ob_source. rww ob_source. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits