silly.v

Require Import Omega.


  Fixpoint silly (n1: nat) (n2:nat) (H: n1 = n2): nat :=
    match H with
      | eq_refl => 0
    end.

  Lemma lem_000:
    forall n,
      1 + n = n + 1.
  intros; omega. Qed.

  Lemma lem_002:
    forall n,
      silly (1+n) (n+1) (lem_000 n) = 0.
  intros; simpl; destruct (lem_000 n);  reflexivity. Qed.

  Lemma lem_003:
    forall a b (H: a = b),
      silly a b H = 0.
  Proof.
    intros.
    simpl. ???