proposition: Lemma target_discrete_nt : forall z a t, target (discrete_nt z a t) = discrete_functor z a (fun x => target (t x)).
proof: Proof. ir. uf discrete_nt. rw Nat_Trans.target_create. tv. Qed.
imports: Arith ordinal nat_trans