proposition: Lemma E_tau_cone_law : Cone_law E_tau.
proof: Proof. unfold Cone_law in |- *; intros x o2 f. elim f. unfold FMor in |- *; simpl in |- *; apply Idr. unfold FMor in |- *; simpl in |- *; apply Idr. unfold FMor in |- *; simpl in |- *. intro i; apply (p (Witness l) i). Qed.
imports: Equalizers PA Limit