lean2/tests/lean/eta_decls.lean.expected.out

to_set_union : ∀ {A} [deceq] s t, @eq (set A) (@ts A (@union A deceq s t)) (@set.union A (@ts A s) (@ts A t))
to_set_empty : ∀ {A}, @eq (set A) (@ts A (@empty A)) (@set.empty A)
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`to_set_union : ∀ {A} [deceq] s t, @eq (set A) (@ts A (@union A deceq s t)) (@set.union A (@ts A s) (@ts A t))`
			`to_set_empty : ∀ {A}, @eq (set A) (@ts A (@empty A)) (@set.empty A)`