theory Fails imports Main begin

inductive reduced :: "bool"  where
 "\<lbrakk>id vs = (n::nat); id t1s = n; t2s = m; id x = [t1s, t2s]\<rbrakk> \<Longrightarrow> reduced"

end