Married.v

Require Import Classical_Prop.
Variable Person : Type.
Variable Jack Anne George : Person.
Variable married : Person -> Prop.
Notation "a ^: b" := (married a /\ ~ married b) (at level 73).
Variable looksAt : Person -> Person -> Prop.
Notation "a ~> b" := (looksAt a b) (at level 72).
Hypothesis cond : Jack ~> Anne /\ Anne ~> George /\ Jack ^: George.
Theorem solution : exists p q : Person, p ~> q /\ p ^: q.
Proof. destruct (classic (married Anne)).
  exists Anne, George. split. apply cond. split. apply H. apply cond.
  exists Jack, Anne. split. apply cond. split. apply cond. apply H. Qed.