Print eq.

Goal 0=1 -> 1=0.

intro.
rewrite H.
Show Proof.
rewrite <- H.
Show Proof.
eapply eq_ind with (2:=H).
split.
Show Proof.
Qed. 



eq_ind
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, x = y -> P y


eq_ind_r
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, y = x -> P y