rewrite_in_hyp.v « failure « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/failure/rewrite_in_hyp.v

blob: 613d707c6cb61cf8cadc56c626d6141e2d3af06e (plain)

1
2
3

Goal forall (T1 T2 : Type) (f:T1 -> Prop) (x:T1) (H:T1=T2), f x -> 0=1.
  intros T1 T2 f x H fx.
  rewrite H in x.