proposition: Lemma expr_leq_weq_ind l leq weq (L: laws l (expr_ind leq weq)) n m (e f: expr n m): (e <==_[l] f -> leq n m e f) /\ (e ==_[l] f -> weq n m e f).
proof: Proof. split; intro H; rewrite <-(expr_ind_eval leq weq e), <-(expr_ind_eval leq weq f); apply (H _ L id). Qed.
imports: kleene syntax