proposition: Lemma Restricted_map_law : Map_law Restricted_fun.
proof: Proof. unfold Map_law in |- *; simpl in |- *. unfold Equal_SubType in |- *; intros a1 a2 H. unfold Restricted_fun in |- *; apply Pres1; trivial. Qed.
imports: Map