proposition: Lemma norm_weq l n m (x: expr n m) {Hl: e_level x ≪ l}: norm x ==_[l] x.
proof: Proof. induction x; simpl norm; simpl e_level in Hl; try reflexivity; rewrite ?pls'pls, ?cap'cap, ?dot'dot, ?itr'itr, ?str'str, ?cnv'cnv, ?e_str' by (rewrite ?norm_level; solve_lower'). apply cup_weq; [apply IHx1|apply IHx2]; solve_lower'. apply cap_weq; [apply IHx1|apply IHx2]; solve_lower'. apply neg_weq, IHx. solve_lower'. apply dot_weq; [apply IHx1|apply IHx2]; solve_lower'. apply itr_weq, IHx. solve_lower'. apply str_weq, IHx. solve_lower'. apply cnv_weq, IHx. solve_lower'. apply ldv_weq; [apply IHx1|apply IHx2]; solve_lower'. apply rdv_weq; [apply IHx1|apply IHx2]; solve_lower'. Qed.
imports: kleene syntax powerfix