iii. H; x:s ` M :t
H ` >=x : s: M :s ! t

iv. H ` M :s ! t H ` N :s
H ` M(N):t

v. H ` M :s H ` N :t
H ` (M;N):s?t

vi. H ` M :s?t
H ` fst(M):s

vii. H ` M :s?t
H ` snd(M):t

2.1.3 Equational Rules

i. (HoeM=N :t)2T
T ` (HoeM=N :t)

ii. T ` (HoeM=N :t) x62dom(HV )
T ` (H; x:soeM=N :t)

iii. T ` (H; x:soeM=N :t) x62FV (M)[FV (N)
T ` (HoeM=N :t)

iv. H ` M :t
T ` (HoeM=N :t)

v. T ` (HoeM=N :t)
T ` (HoeN=M :t)

vi. T ` (HoeL=M :t) T ` (HoeM=N :t)
T ` (HoeL=M :t)

vii. T ` (HoeM=M :s!t) T ` (HoeN=N :s
T ` (HoeM(N)=M (N ):t)

viii. T ` (H; x:soeM=N :t)
T ` (Hoe>=x : s: M=>=x : s: N :s!t

ix. H; x:s ` M :t H ` N :s
T ` (Hoe(>=x : s: M)(N)=[N=x]M :t

x. H ` M :s!t x62FV (M)
T ` (Hoe>=x : s: M(x)=M :s!t

xi. H ` M :s H ` N :t
T ` (Hoefst(M;N)=M :s

xii. H ` M :s H ` N :t
T ` (Hoesnd(M;N)=N :t

xiii. H ` M :s?t
T ` (Hoe(fst(M);snd(N))=M :s?t

Rules vii and viii assert that abstraction and application are congruence relations relative to a fixed theory while rules ix and x are respectively the reduction and extensionality rules.