2814.v « opened « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/opened/2814.v

blob: d8f6b906a1e49ce0fc40d79b03c673c9dda2316d (plain)

Require Import Program.

Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
  intros.
  induction H.