var a : Type; b : Type

free type Pair(a : Type)(b : Type) ::= Pair (fst : a; snd : b)

op f : forall a : Type; b : Type .

a_v-1 * b_v-2 ->? Pair a_v-1 b_v-2

= \ (var a : a, var b : b)

.! (((op Pair[a_v1; b_v2]

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2) :

a_v1 * b_v2 -> Pair a_v1 b_v2)

(var a : a, var b : b) :

Pair a_v1 b_v2) as

Pair a_v1 b_v2

op g : Pair a b ->? a

program ((op g[_var_17_v17; _var_19_v19]

: forall a : Type; b : Type . Pair a_v-1 b_v-2 ->? a_v-1) :

Pair _var_17_v17 _var_19_v19 ->? _var_17_v17)

(((op Pair[_var_17_v17; _var_19_v19]

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2) :

_var_17_v17 * _var_19_v19 -> Pair _var_17_v17 _var_19_v19)

(var a : _var_17_v17, var b : _var_19_v19) :

Pair _var_17_v17 _var_19_v19) :

_var_17_v17

= (var a : _var_17_v17)

%% Type Constructors -----------------------------------------------------

Logical : Type := Unit ->? Unit

Pair

: Type -> Type -> Type

%[free type Pair(a : Type)(b : Type)

::= Pair : a_v-1 * b_v-2 -> Pair a_v-1 b_v-2

(fst : a_v-1; snd : b_v-2)]%

Pred : Type -> Type := \ a : Type . a_v-1 ->? Unit

Unit : Type

__*__ : +Type -> +Type -> Type

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

__-->?__ : -Type -> +Type -> Type < __->?__

__->__ : -Type -> +Type -> Type < __->?__

__->?__ : -Type -> +Type -> Type

a : Type %(var_1)%

b : Type %(var_2)%

%% Assumptions -----------------------------------------------------------

Pair

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2

%(construct Pair)%

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

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

__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__

: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

bottom : forall a : Type . a_v-1 %(fun)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

f : forall a : Type; b : Type . a_v-1 * b_v-2 ->? Pair a_v-1 b_v-2

%(op)%

= \ (var a : a, var b : b)

.! (((op Pair[a_v1; b_v2]

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2) :

a_v1 * b_v2 -> Pair a_v1 b_v2)

(var a : a, var b : b) :

Pair a_v1 b_v2) as

Pair a_v1 b_v2

false : Unit %(fun)%

fst

: forall a : Type; b : Type . Pair a_v-1 b_v-2 -> a_v-1

%(select from Pair constructed by

Pair : forall a : Type; b : Type .

a_v-1 * b_v-2 -> Pair a_v-1 b_v-2)%

g : forall a : Type; b : Type . Pair a_v-1 b_v-2 ->? a_v-1 %(op)%

not__ : ? Unit ->? Unit %(fun)%

snd

: forall a : Type; b : Type . Pair a_v-1 b_v-2 -> b_v-2

%(select from Pair constructed by

Pair : forall a : Type; b : Type .

a_v-1 * b_v-2 -> Pair a_v-1 b_v-2)%

true : Unit %(fun)%

�__ : ? Unit ->? Unit %(fun)%

%% Sentences -------------------------------------------------------------

forall a : Type; b : Type; x_1_1 : a_v-1; x_1_2 : b_v-2

. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op fst : forall a : Type; b : Type . Pair a_v-1 b_v-2 -> a_v-1)

((op Pair

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2)

(var x_1_1 : a_v-1, var x_1_2 : b_v-2)),

var x_1_1 : a_v-1) %(ga_select_fst)%

forall a : Type; b : Type; x_1_1 : a_v-1; x_1_2 : b_v-2

. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op snd : forall a : Type; b : Type . Pair a_v-1 b_v-2 -> b_v-2)

((op Pair

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2)

(var x_1_1 : a_v-1, var x_1_2 : b_v-2)),

var x_1_2 : b_v-2) %(ga_select_snd)%

free type Pair(a : Type)(b : Type)

::= Pair : a_v-1 * b_v-2 -> Pair a_v-1 b_v-2

(fst : a_v-1; snd : b_v-2) %(ga_Pair)%

forall a : a; b : b

. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op f

: forall a : Type; b : Type . a_v-1 * b_v-2 ->? Pair a_v-1 b_v-2)

(var a : a, var b : b),

(((op Pair[a_v1; b_v2]

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2) :

a_v1 * b_v2 -> Pair a_v1 b_v2)

(var a : a, var b : b) :

Pair a_v1 b_v2) as

Pair a_v1 b_v2) %(def_f)%

program ((op g[_var_17_v17; _var_19_v19]

: forall a : Type; b : Type . Pair a_v-1 b_v-2 ->? a_v-1) :

Pair _var_17_v17 _var_19_v19 ->? _var_17_v17)

(((op Pair[_var_17_v17; _var_19_v19]

: forall a : Type; b : Type . a_v-1 * b_v-2 -> Pair a_v-1 b_v-2) :

_var_17_v17 * _var_19_v19 -> Pair _var_17_v17 _var_19_v19)

(var a : _var_17_v17, var b : _var_19_v19) :

Pair _var_17_v17 _var_19_v19) :

_var_17_v17

= (var a : _var_17_v17) %(pe_g)%