blob: 31e7861de4c993f4c05ed46d98c9a9a3235901ff (
plain)
1
2
3
4
5
6
7
|
Require Import FunctionalExtensionality.
Goal forall y, @f_equal = y.
intro.
apply functional_extensionality_dep.
(* Error: Ill-typed evar instance in HoTT/coq, Anomaly: Uncaught exception Reductionops.NotASort(_). Please report. before that. *)
Abort.
|
