The Coq mailing list

[Geoff Reedy <geoff AT programmer-monk.net>]

On Wed, Aug 21, 2013 at 08:43:58PM +0000, t x said
> I believe the process I want is called "beta expansion". Is there a way to
> fix type_rewrite so that line 14 behaves like line 32?

Beta expansion is what the pattern tactic does. I don't think there's a
a way to get what you want from Gallina without applying that tactic in
either the goal or the assumptions. Maybe you can write a tactic to
figure it out.

To show how the pattern tactic can be applied here, if you change 
type_rewrite to

Definition type_rewrite {T : type} {Ht : T -> Type} {x y : T} (t : Ht x)
        (H : x = y) := @eq_rect _ x (fun i => _) t y H.

then the proof scripts

intros a b H Heq.
pattern a in H.
pose proof (type_rewrite H Heq) as H2.
simpl in H2.
assumption.

and

intros a b H Heq.
pattern b at 1.
apply (type_rewrite H Heq).

go through. Not sure at all if this is useful to you.

-- Geoff