Nuprl Definition : fl-eq
(x==y) == free-dml-deq(names(I);NamesDeq) x y
Definitions occuring in Statement :
names-deq: NamesDeq,
names: names(I),
free-dml-deq: free-dml-deq(T;eq),
apply: f a
Definitions occuring in definition :
apply: f a,
free-dml-deq: free-dml-deq(T;eq),
names: names(I),
names-deq: NamesDeq
FDL editor aliases :
fl-eq
Latex:
(x==y) == free-dml-deq(names(I);NamesDeq) x y
Date html generated:
2016_05_18-PM-00_09_39
Last ObjectModification:
2015_11_07-PM-01_55_47
Theory : cubical!type!theory
Home
Index