header {* Very Simple Predicate Logic with Equality *} theory VSPredEq imports VSPred begin axiomatization "eq" :: "'a=> 'a=> o" (infix "=" 50) where refl: "x= x" and sym: "x= y ==> y= x" and trans: "[| x= y; y= z |] ==> x= z" and cong: "x= y ==> f x= f y" and subst: "[| x= y; P x |] ==> P y" end