Josh Cough is Awesome

Josh.v

Require Import Coq.Strings.String.
Require Export "Prop".
Require Export "Logic".

Inductive person: Type := personc : string -> string -> person.

Definition jc: person := personc "Josh" "Cough".

Inductive awesome : person -> Prop := | ajc : awesome jc.

Theorem josh_cough_is_awesome : awesome jc. Proof. apply ajc. Qed.

Definition is_josh_cough (p:person) : Prop := p = jc.

Theorem only_josh_cough_is_awesome : forall p : person,
  (is_josh_cough p -> awesome p) /\ (~ is_josh_cough p -> ~ awesome p).
Proof.
  intros.
  split.
  Case "Josh Cough".
    intros.
    inversion H.
    apply josh_cough_is_awesome.
  Case "Any other human ever.".
    unfold not.
    intros.
    unfold is_josh_cough in H.
    inversion H0. 
    unfold jc in H.
    rewrite H1 in H.
    apply H. 
    reflexivity.
Qed.
  

This is a good example of how hard it is to get definitions right :)