# basic_rewrites();;
val it : thm list =
[|- FST (x,y) = x; |- SND (x,y) = y; |- FST x,SND x = x;
|- (if x = x then y else z) = y; |- (if T then t1 else t2) = t1;
|- (if F then t1 else t2) = t2; |- ~ ~t <=> t; |- ~T <=> F; |- ~F <=> T;
|- (@y. y = x) = x; |- x = x <=> T; |- (T <=> t) <=> t;
|- (t <=> T) <=> t; |- (F <=> t) <=> ~t; |- (t <=> F) <=> ~t; |- ~T <=> F;
|- ~F <=> T; |- T /\ t <=> t; |- t /\ T <=> t; |- F /\ t <=> F;
|- t /\ F <=> F; |- t /\ t <=> t; |- T \/ t <=> T; |- t \/ T <=> T;
|- F \/ t <=> t; |- t \/ F <=> t; |- t \/ t <=> t; |- T ==> t <=> t;
|- t ==> T <=> T; |- F ==> t <=> T; |- t ==> t <=> T; |- t ==> F <=> ~t;
|- (!x. t) <=> t; |- (?x. t) <=> t; |- (\x. f x) y = f y;
|- x = x ==> p <=> p]