subst.dk 298 Bytes
Newer Older
Guillaume GENESTIER's avatar
Guillaume GENESTIER committed
1 2 3 4 5
#NAME subst.

A : Type.
x : A.
t : (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => A) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x.