proposition: Lemma clean_leq_weq_0 l: l ≪ BOT+CKA -> forall n m (x y: expr n m), (x <==_[l] y -> clean y = 0%ast -> clean x = 0%ast) /\ (x ==_[l] y -> (clean x = 0%ast <-> clean y = 0%ast)).
proof: Proof. intros Hl. apply expr_leq_weq_ind. constructor; [constructor; [constructor|..] |..]; simpl ob in *; discr_levels Hl idtac; intro_vars; destruct_tests; intuition (congruence || discriminate). Qed.
imports: kleene syntax