# basic_congs();;
val it : thm list =
[|- (!x. x IN s ==> f x = g x) ==> sum s (\i. f i) = sum s g;
|- (!i. a <= i /\ i <= b ==> f i = g i)
==> sum (a..b) (\i. f i) = sum (a..b) g;
|- (!x. p x ==> f x = g x) ==> sum {y | p y} (\i. f i) = sum {y | p y} g;
|- (!x. x IN s ==> f x = g x) ==> nsum s (\i. f i) = nsum s g;
|- (!i. a <= i /\ i <= b ==> f i = g i)
==> nsum (a..b) (\i. f i) = nsum (a..b) g;
|- (!x. p x ==> f x = g x) ==> nsum {y | p y} (\i. f i) = nsum {y | p y} g;
|- (g <=> g')
==> (g' ==> t = t')
==> (~g' ==> e = e')
==> (if g then t else e) = (if g' then t' else e');
|- (p <=> p') ==> (p' ==> (q <=> q')) ==> (p ==> q <=> p' ==> q')]