proposition: Theorem erase_faithful_leq l n m (x y: expr n m): e_level x + e_level y ≪ l -> l ≪ BOT+CKA -> erase l x <==_[l] erase l y -> x <==_[l] y.
proof: Proof. intros Hxy Hl H. rewrite <-(clean_weq x), <-(clean_weq y) by solve_lower'. destruct (clean_spec x) as [Hx|Hx]. rewrite <-Hl; solve_lower'. rewrite Hx. rewrite <-clean_0_level in Hxy by assumption. lattice. destruct (clean_spec y) as [Hy|Hy]. rewrite <-Hl; solve_lower'. rewrite Hy. apply clean_leq_0 in H. rewrite (clean_erase l l) in H. apply erase_0 in H. now rewrite H. assumption. now rewrite (clean_erase l l), Hy. set (l' := mk_level (has_cup l) false (has_cap l) (has_top l) (has_str l) (has_cnv l) (has_neg l) (has_div l)). assert (L: l' ≪ l). rewrite lower_spec. intuition discriminate. assert (L': l ≪ BOT+l'). rewrite lower_spec. simpl. intuition. assert (G: clean x <==_[l'] clean y). apply erase_faithful_leq_clean. assumption. assumption. rewrite <-L in Hl. apply Hl. rewrite <-2(clean_erase l l'). destruct (fun Hl => clean_factorise_leq Hl (e_leq_weaken H)) as [H'|H']. now rewrite L. rewrite (clean_erase l l) in H'. apply erase_0 in H'. rewrite H' in Hx. inversion Hx. assumption. apply e_leq_weaken, G. Qed.
imports: kleene syntax