proposition: Lemma lhs_ok l r ( h : rule l r) : l = apps (Fun (lhs_fun h)) (lhs_args h).
proof: Proof. inversion h; subst; refl. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec) CoLoR(VecUtil) CoLoR(LCompRewrite)