fact: Definition glang_inj (n: traces_unit) (x: expr_ops (ord pred) BL): traces Atom := fun w => match w with | tnil a => is_true (eval (set.mem a) x) | _ => False end.
imports: traces kat lsyntax ordinal comparisons boolean