proposition: Lemma clean_spec n m (x: expr n m): e_level x ≪ BOT+CKA -> clean x = 0%ast \/ is_clean (clean x).
proof: Proof. induction x; simpl e_level; simpl clean; unfold e_pls', e_dot', e_itr', e_str', e_cnv'; simpl is_clean; try intuition discriminate_levels. intro Hl. destruct IHx1 as [->|IHx1]. solve_lower'. apply IHx2. solve_lower'. rewrite is_zer_clean by assumption. destruct IHx2 as [->|IHx2]. solve_lower'. now right. rewrite is_zer_clean by assumption. right; now split. intro Hl. destruct IHx1 as [->|IHx1]. solve_lower'. now left. rewrite is_zer_clean by assumption. destruct IHx2 as [->|IHx2]. solve_lower'. now left. rewrite is_zer_clean by assumption. right; now split. intro Hl. destruct IHx as [->|IHx]. solve_lower'. now left. rewrite is_zer_clean by assumption. now right. intro Hl. destruct IHx as [->|IHx]. solve_lower'. now right. rewrite is_zer_clean by assumption. simpl. tauto. intro Hl. destruct IHx as [->|IHx]. solve_lower'. now left. rewrite is_zer_clean by assumption. now right. Qed.
imports: kleene syntax