1	import Base
2	
3	# Applying a two-argument function to equal arguments gives equal results.
4	law cong2:
5	  for -A: Type
6	  for -B: Type
7	  for -C: Type
8	  for -f: A -> B -> C
9	  for -a1: A
10	  for -a2: A
11	  for -b1: B
12	  for -b2: B
13	  for ea: {a1 == a2 : A}
14	  for eb: {b1 == b2 : B}
15	  {f(a1, b1) == f(a2, b2) : C}
16	
17	def cong2(A, B, C, f, a1, a2, b1, b2, ea, eb):
18	  %ea : {f(a1, b1) == f(_, b2) : C}
19	  %eb : {f(a1, b1) == f(a1, _) : C}
20	  {==}
21	
22	# If a equals b, any property of a is also a property of b.
23	law subst:
24	  for -A: Type
25	  for -P: A -> Type
26	  for -a: A
27	  for -b: A
28	  for e: {a == b : A}
29	  for p: P(a)
30	  P(b)
31	
32	def subst(A, P, a, b, e, p):
33	  %e : P(_)
34	  p
35	
36	# Equality chains through three steps: a = b, b = c and c = d give a = d.
37	law trans3:
38	  for -A: Type
39	  for -a: A
40	  for -b: A
41	  for -c: A
42	  for -d: A
43	  for ab: {a == b : A}
44	  for bc: {b == c : A}
45	  for cd: {c == d : A}
46	  {a == d : A}
47	
48	def trans3(A, a, b, c, d, ab, bc, cd):
49	  %cd : {a == _ : A}
50	  %bc : {a == _ : A}
51	  ab
52	
53	# Equal naturals have equal successors.
54	law cong_succ:
55	  for -a: Nat
56	  for -b: Nat
57	  for e: {a == b : Nat}
58	  {1n+a == 1n+b : Nat}
59	
60	def cong_succ(a, b, e):
61	  %e : {1n+a == 1n+_ : Nat}
62	  {==}