proposition: Lemma PhiCone_1_map_law : Map_law0'' PhiCone_1_fun.
proof: Proof. unfold Map_law0'', PhiCone_1_fun in |- *. intros f g H; simpl in |- *. unfold Equal_NT in |- *; simpl in |- *. unfold PhiCone_1_fun_tau in |- *; intro i. apply Comp_r; trivial. Qed.
imports: SET Limit Map0_dup1