{T}

eq1 TT

x:T. eq1(x,x)

x,y:T. eq1(x,y) eq1(y,x)

x,y,z:T. eq1(x,y) eq1(y,z) eq1(x,z)

{T}

eq2 TT

x:T. eq2(x,x)

x,y:T. eq2(x,y) eq2(y,x)

x,y,z:T. eq2(x,y) eq2(y,z) eq2(x,z)

{T}

eq3 TT

x:T. eq3(x,x)

x,y:T. eq3(x,y) eq3(y,x)

x,y,z:T. eq3(x,y) eq3(y,z) eq3(x,z)

eq1 = eq2 {T}

eq2 = eq3 {T}

L1(eq3)L2

L2(eq3)L3

L1(eq3)L3

RenameVar `eq' 13
THEN
OnHyps [22;21;12;11;10;9;8;7;6;5;4;3] (i.Thin i)

1	3. eq: {T} 4. eq TT 5. x:T. eq(x,x) 6. x,y:T. eq(x,y) eq(y,x) 7. x,y,z:T. eq(x,y) eq(y,z) eq(x,z) 8. L1: T List 9. L2: T List 10. L3: T List 11. L1(eq)L2 12. L2(eq)L3 L1(eq)L3

About: