Variable Personne : Set.
Variable dans_la_maison : Personne -> Prop.
Variable a_tue : Personne -> Personne -> Prop.
Variable deteste : Personne -> Personne -> Prop.
Variable plus_riche_que : Personne -> Personne -> Prop.
Variable Agatha, Majordome, Charles : Personne.

Axiom meurtre : (EX x:Personne | (dans_la_maison x) /\ (a_tue x Agatha)).
Axiom Agatha_la : (dans_la_maison Agatha).
Axiom Majordome_la : (dans_la_maison Majordome).
Axiom Charles_la : (dans_la_maison Charles).
Axiom presents : (x:Personne) (dans_la_maison x) ->
                              x=Agatha \/ x=Majordome \/ x=Charles.
Axiom haine : (y,x:Personne) (a_tue x y) -> (deteste x y).
Axiom fortune : (y,x:Personne) (a_tue x y) -> ~(plus_riche_que x y).
Axiom Agatha_et_Charles : (x:Personne) (deteste Agatha x) -> ~(deteste Charles x).
Axiom Agatha_deteste_presque_tout_le_monde : (x:Personne) ~x=Majordome -> (deteste Agatha x).
Axiom Majordome_condescendant : (x:Personne) ~(plus_riche_que x Agatha) -> (deteste Majordome x).
Axiom Majordome_fidele : (x:Personne) (deteste Agatha x) -> (deteste Majordome x).
Axiom il_y_a_de_l_espoir : (x:Personne) (EX y:Personne | (dans_la_maison y) /\ ~(deteste x y)).
Axiom faut_pas_confondre : ~(Agatha=Majordome).

Lemma mais_c_est_bien_sur : (a_tue Agatha Agatha).
Proof.
  Cut (deteste Agatha Agatha). Intro.
  Elim meurtre. Intros. Elim H0. Intros. Elim (presents x). Intro. Rewrite H3 in H2. Assumption.
  Intro. Elim H3. Intro. Rewrite H4 in H2. Cut (deteste Majordome Agatha). Intro.
  Cut ~(plus_riche_que Majordome Agatha). Intro. Cut (deteste Majordome Majordome). Intro.
  Cut ~Agatha=Charles. Intro. Cut (deteste Agatha Charles). Intro. Cut (deteste Majordome Charles).
  Intro. Elim (il_y_a_de_l_espoir Majordome). Intros. Elim H11. Intros. Elim (presents x0).
  Intro. Absurd (deteste Majordome x0). Assumption.
  Rewrite H14. Assumption.
  Intro. Elim H14. Intro. Absurd (deteste Majordome x0). Assumption.
  Rewrite H15. Assumption.
  Intro. Absurd (deteste Majordome x0). Assumption.
  Rewrite H15. Assumption.
  Assumption.
  Apply Majordome_fidele. Assumption.
  Apply Agatha_deteste_presque_tout_le_monde. Unfold not. Intro. Absurd (deteste Charles Agatha).
  Apply Agatha_et_Charles. Assumption.
  Rewrite H9. Assumption.
  Unfold not. Intro. Absurd (deteste Charles Agatha). Apply Agatha_et_Charles. Assumption.
  Rewrite <- H8. Assumption.
  Apply Majordome_condescendant. Assumption.
  Apply fortune. Assumption.
  Apply haine. Assumption.
  Intro. Rewrite H4 in H2. Absurd (deteste Charles Agatha). Apply Agatha_et_Charles. Assumption.
  Apply haine. Assumption.
  Assumption.
  Apply Agatha_deteste_presque_tout_le_monde. Exact faut_pas_confondre.
Qed.