{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}

HypSubst 22 24 THENA Equivalence -1 THEN HypSubst 23 24 THENA Equivalence -1 THEN HypSubst 23 25 THENA Equivalence -1
THEN
RenameVar `eq' 14
THEN
OnHyps [23;22;13;12;11;10;9;8;7;6;5;4] (i.Thin i)

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

About: