(*
  The omitted proof in problem 11.2.2
  It is formulated in Coq , the translation into a ND proof is straightforward however.
 *)

(* We work in a domain U *)
Parameter U : Set.
(* A Role is a binary relation;
   In Coq this corresponds to a binary¹ function into [Prop].

 ¹: We use currying here. ((A × B) → C ≅ A → B → C)
 *)
Parameter R : U -> U -> Prop.

(* Concepts are just unary predicates. *)
Parameters C D : U -> Prop.


(* Our two propositions: *)
Definition C_1 (X : U) : Prop :=
  forall Y, R X Y -> C Y /\ D Y.

Definition C_2 (X : U) : Prop :=
  (forall Y, R X Y -> C Y) /\ (forall Y, R X Y -> D Y).


(* Now we prove the equivalence *)
Theorem equiv : forall X, C_1 X <-> C_2 X.
  intros X.
  split.
  - intros H. split.
    + intros Y HR.
      unfold C_1 in H.
      specialize (H Y HR).
      destruct H as [Hl Hr].
      assumption.
    + intros Y HR.
      unfold C_1 in H.
      specialize (H Y HR).
      destruct H as [Hl Hr].
      assumption.
  - intros H.
    unfold C_2 in H.
    destruct H as [Hl Hr].
    unfold C_1.
    intros Y HR.
    split.
    + specialize (Hl Y HR).
      assumption.
    + specialize (Hr Y HR).
      assumption.
  Show Proof. (* This roughly corresponds to the proof tree in ND *)
  (* We are done here, but the proof is quite lengthy *)
  Restart. (* Let's try again *)
  firstorder. (* That was quick! *)
Qed.