f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichtype t

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederop f : ? t -> t

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maederop g : t -> (? t)

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederops a, b : t

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanuops c, d : ? t

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski. f a = g c;

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder%% Type Constructors -----------------------------------------------------

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskit : Type

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski%% Assumptions -----------------------------------------------------------

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedera : t %(op)%

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederb : t %(op)%

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederc : ? t %(op)%

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederd : ? t %(op)%

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederf : ? t -> t %(op)%

da955132262baab309a50fdffe228c9efe68251dCui Jiang : t -> ? t %(op)%

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder%% Sentences -------------------------------------------------------------

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederf a = g c

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder