By: |
let T
let Rewrite by
let Thm* f:(A A A), u:A.
let Thm* is_ident(A; f; u)
let Thm* 
let Thm* is_assoc_sep(A; f)
let Thm* 
let Thm* ( a,c,b: , e:({a..b } A).
let Thm* (a c
let Thm* (
let Thm* (c b
let Thm* (
let Thm* ((Iter(f;u) i:{a..b }. e(i))
let Thm* (=
let Thm* (f((Iter(f;u) i:{a..c }. e(i)),Iter(f;u) i:{c..b }. e(i))) in
T Using:[a:= a | c:= c] THEN T Using:[a:= c | c:= d] |