proposition: Lemma SET_diese1_tau_cone_law : Cone_law SET_diese1_tau.
proof: Proof. unfold Cone_law in |- *; intros i j g; simpl in |- *. unfold Ext in |- *; simpl in |- *. intro a; elim a; simpl in |- *. unfold Comp_fun in |- *; simpl in |- *. apply (EqC tau g x). Qed.
imports: SET Single Limit Map0_dup1