proposition: Lemma FunDiscr_map_law : forall i j : I, Map_law (FunDiscr_arrow (i:=i) (j:=j)).
proof: Proof. unfold Map_law in |- *. intros i j f; elim f; intros k f1 H. apply (Discr_mor_ind1 (P:=fun f1 : Discr_mor k k => FunDiscr_arrow (Build_Discr_mor k) =_S FunDiscr_arrow f1)). simpl in |- *; apply Refl. Qed.
imports: Limit Discr Products