5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertype t

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop f : ? t -> t

1a6464613c59e35072b90ca296ae402cbe956144Christian Maederop g : t -> (? t)

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop a, b : t

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop c, d : ? t

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder. (fun __=__[t] : forall a : Type . a * a ->? Unit)

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (((op f : ? t -> t) (op a : t), (op g : t -> ? t) (op c : ? t)))

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% Type Constructors -----------------------------------------------------

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder? : +Type -> Type

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLogical : Type := ? Unit

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederUnit : Type

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__*__ : +Type -> +Type -> Type

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__*__*__ : +Type -> +Type -> +Type -> Type

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

09a67ca9b5cdf09e06470d4c965484783e2963f4Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__->__ : -Type -> +Type -> Type < __->?__

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__->?__ : -Type -> +Type -> Type

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedert : Type

d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder%% Assumptions -----------------------------------------------------------

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers__=__ : forall a : Type . a * a ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl__if__ : ? Unit * ? Unit ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedera : t %(op)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederb : t %(op)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederbottom : forall a : Type . a %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederc : ? t %(op)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederd : ? t %(op)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederf : ? t -> t %(op)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederfalse : Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederg : t -> ? t %(op)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedernot__ : ? Unit ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedertrue : Unit %(fun)%

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers�__ : ? Unit ->? Unit %(fun)%

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder%% Sentences -------------------------------------------------------------

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder(f (a)) = (g (c))

8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers