ho_bug2.dk 195 Bytes
Newer Older
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14
#NAME bug.

A : Type.

def F : (A -> A) -> A -> A.

a : A.
[f] F (x => f x) _ --> a.

g : A -> A.
def test (b : A) := F (x => g x) b.

#SNF test.
#CONV test, b : A => a. (; Answer must be YES ;)