proposition: Lemma cnv'cnv l n m (x: expr n m) {Hl: CNV+e_level x ≪ l}: cnv' x ==_[l] x°.
proof: Proof. symmetry. induction x; simpl cnv'; simpl e_level in Hl; rewrite ?dot'dot, ?e_str' by (rewrite ?cnv'_level; solve_lower'). apply cnv0. apply cnvtop. apply cnv1. rewrite cnvpls. apply cup_weq; [apply IHx1|apply IHx2]; solve_lower'. rewrite cnvcap. apply cap_weq; [apply IHx1|apply IHx2]; solve_lower'. rewrite cnvneg. apply neg_weq, IHx. solve_lower'. rewrite cnvdot. apply dot_weq; [apply IHx2|apply IHx1]; solve_lower'. rewrite cnvitr. apply itr_weq, IHx. solve_lower'. rewrite cnvstr. apply str_weq, IHx. solve_lower'. apply cnv_invol. rewrite cnvldv. apply rdv_weq; [apply IHx1|apply IHx2]; solve_lower'. rewrite cnvrdv. apply ldv_weq; [apply IHx1|apply IHx2]; solve_lower'. reflexivity. Qed.
imports: kleene syntax powerfix