+qed.
+
+theorem t: 0=0 \to stupidtype.
+ intros; constructor 1.
+qed.
+
+(* In this test "elim t" should open a new goal 0=0 and put it in the *)
+(* goallist so that the THEN tactical closes it using reflexivity. *)
+theorem foo: let ax \def refl_equal ? 0 in t ax = t ax.
+ elim t; reflexivity.
+qed.